From 3c279293b9ef9c694629917815bc1913b500417a Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 17 May 2023 15:43:51 -0400
Subject: [PATCH] Define preorder-enriched cats, refl. graph of preorder
 enriched cats

---
 .../PreorderEnriched/PreorderEnriched.agda    | 33 ++++++++
 .../Cubical/HigherCategories/RGPEC.agda       | 77 +++++++++++++++++++
 .../gradual-typing-sgdt.agda-lib              |  1 +
 3 files changed, 111 insertions(+)
 create mode 100644 formalizations/guarded-cubical/Cubical/HigherCategories/PreorderEnriched/PreorderEnriched.agda
 create mode 100644 formalizations/guarded-cubical/Cubical/HigherCategories/RGPEC.agda

diff --git a/formalizations/guarded-cubical/Cubical/HigherCategories/PreorderEnriched/PreorderEnriched.agda b/formalizations/guarded-cubical/Cubical/HigherCategories/PreorderEnriched/PreorderEnriched.agda
new file mode 100644
index 0000000..8f4afff
--- /dev/null
+++ b/formalizations/guarded-cubical/Cubical/HigherCategories/PreorderEnriched/PreorderEnriched.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --safe #-}
+module Cubical.HigherCategories.PreorderEnriched.PreorderEnriched where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Relation.Binary.Base
+
+private
+  variable
+    â„“ â„“' â„“'' â„“c â„“c' â„“c'' â„“d â„“d' â„“d'' : Level
+
+open BinaryRelation
+open Category
+
+record PreorderEnrichedCategory â„“ â„“' â„“'' : Type (â„“-suc (â„“-max â„“ (â„“-max â„“' â„“''))) where
+  field
+    cat : Category â„“ â„“'
+    _≤_ : ∀ {x y} → cat [ x , y ] → cat [ x , y ] → Type ℓ''
+    isProp≤ : ∀ x y (f g : cat [ x , y ]) → isProp (f ≤ g)
+    isReflexive : ∀ {x y} → isRefl (_≤_ {x}{y})
+    isTransitive : ∀ {x y} → isTrans (_≤_ {x}{y})
+
+    isMonotone⋆ : ∀ {x y z} {f f' : cat [ x , y ]}{g g' : cat [ y , z ]}
+                → f ≤ f' → g ≤ g'
+                → (f ⋆⟨ cat ⟩ g) ≤ (f' ⋆⟨ cat ⟩ g')
+
+open PreorderEnrichedCategory
+
+record PreorderEnrichedFunctor (C : PreorderEnrichedCategory â„“c â„“c' â„“c'') (D : PreorderEnrichedCategory â„“d â„“d' â„“d'') : Type (â„“-suc (â„“-max (â„“-max (â„“-max â„“c â„“c') â„“c'') (â„“-max (â„“-max â„“d â„“d') â„“d''))) where
+  field
+    functor : Functor (C .cat) (D .cat)
+    isMonotoneF : ∀ {x y} (f f' : C .cat [ x , y ]) → C ._≤_ f f' → D ._≤_ (functor ⟪ f ⟫) (functor ⟪ f' ⟫)
diff --git a/formalizations/guarded-cubical/Cubical/HigherCategories/RGPEC.agda b/formalizations/guarded-cubical/Cubical/HigherCategories/RGPEC.agda
new file mode 100644
index 0000000..e5a92c5
--- /dev/null
+++ b/formalizations/guarded-cubical/Cubical/HigherCategories/RGPEC.agda
@@ -0,0 +1,77 @@
+{-# OPTIONS --safe #-}
+-- Reflexive graph of preorder enriched categories
+module Cubical.HigherCategories.RGPEC where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Relation.Binary.Base
+
+open import Cubical.HigherCategories.PreorderEnriched.PreorderEnriched
+
+private
+  variable
+    â„“ â„“' â„“'' â„“''' â„“c â„“c' â„“c'' â„“d â„“d' â„“d'' : Level
+
+open BinaryRelation
+open Category
+open PreorderEnrichedCategory
+
+-- Notation note: l, r stand for left, right and t, m, b stand for top, middle, bottom
+-- We visualize these squares having the morphisms of the pe-cat be
+-- vertical and the Rels being horizontal
+record RGPEC â„“ â„“' â„“'' â„“''' â„“'''' : Type (â„“-suc (â„“-max â„“ (â„“-max â„“' (â„“-max â„“'' (â„“-max â„“''' â„“''''))))) where
+  field
+    pe-cat : PreorderEnrichedCategory â„“ â„“' â„“''
+    HRel : ∀ (x y : pe-cat .cat .ob) → Type ℓ'''
+    Sq : ∀ {xtl xtr xbl xbr : pe-cat .cat .ob}
+        → (Rt : HRel xtl xtr)
+        → (fl : pe-cat .cat [ xtl , xbl ])
+        → (fr : pe-cat .cat [ xtr , xbr ])
+        → (Rb : HRel xbl xbr)
+        → Type ℓ''''
+    -- Could drop this but more laws
+    isPropSq : ∀ {xtl xtr xbl xbr}
+        → (Rt : HRel xtl xtr)
+        → (fl : pe-cat .cat [ xtl , xbl ])
+        → (fr : pe-cat .cat [ xtr , xbr ])
+        → (Rb : HRel xbl xbr)
+        → isProp (Sq Rt fl fr Rb)
+    IdRel : ∀ {x} → HRel x x
+    idSq : ∀ {xl xr} → (R : HRel xl xr) → Sq R (pe-cat .cat .id) (pe-cat .cat .id) R
+    _⋆Sq_ : ∀ {xtl xtr xml xmr xbl xbr}
+          → {Rt : HRel xtl xtr}
+          → {ftl : pe-cat .cat [ xtl , xml ]}
+          → {ftr : pe-cat .cat [ xtr , xmr ]}
+          → {Rm : HRel xml xmr}
+          → {fbl : pe-cat .cat [ xml , xbl ]}
+          → {fbr : pe-cat .cat [ xmr , xbr ]}
+          → {Rb : HRel xbl xbr}
+          → (St : Sq Rt ftl ftr Rm)
+          → (Sb : Sq Rm fbl fbr Rb)
+          → Sq Rt (ftl ⋆⟨ pe-cat .cat ⟩ fbl) (ftr ⋆⟨ pe-cat .cat ⟩ fbr) Rb
+    reflSq : ∀ {xt xb} (f : pe-cat .cat [ xt , xb ]) → Sq IdRel f f IdRel
+    transSqL : ∀ {xtl xtr xbl xbr}
+        → {Rt : HRel xtl xtr}
+        → {fl : pe-cat .cat [ xtl , xbl ]}
+        → {fl' : pe-cat .cat [ xtl , xbl ]}
+        → {fr : pe-cat .cat [ xtr , xbr ]}
+        → {Rb : HRel xbl xbr}
+        → (Sq Rt fl fr Rb)
+        → pe-cat ._≤_ fl' fl
+        → (Sq Rt fl' fr Rb)
+    transSqR : ∀ {xtl xtr xbl xbr}
+        → {Rt : HRel xtl xtr}
+        → {fl : pe-cat .cat [ xtl , xbl ]}
+        → {fr : pe-cat .cat [ xtr , xbr ]}
+        → {fr' : pe-cat .cat [ xtr , xbr ]}
+        → {Rb : HRel xbl xbr}
+        → (Sq Rt fl fr Rb)
+        → pe-cat ._≤_ fr fr'
+        → (Sq Rt fl fr' Rb)
+
+    -- This is like a form of univalence: We know f ≤ g ⇒ Sq Id f g Id
+    -- (by refl & trans) and this requires that to be an equivalence
+    identity-extension : ∀ {x y : pe-cat .cat .ob} → (f g : pe-cat .cat [ x , y ])
+                       → Sq IdRel f g IdRel → pe-cat ._≤_ f g
diff --git a/formalizations/guarded-cubical/gradual-typing-sgdt.agda-lib b/formalizations/guarded-cubical/gradual-typing-sgdt.agda-lib
index 090c97f..ddf815f 100644
--- a/formalizations/guarded-cubical/gradual-typing-sgdt.agda-lib
+++ b/formalizations/guarded-cubical/gradual-typing-sgdt.agda-lib
@@ -1,3 +1,4 @@
 name: gradual-typing-sgdt
 include: .
 depend: cubical
+flags: --cubical
\ No newline at end of file
-- 
GitLab