Add definition of a section of a displayed category

maxsnew · Jul 1, 2023 · f4f8b74 · f4f8b74
1 parent 1cbbf47
commit f4f8b74
Showing 1 changed file with 27 additions and 3 deletions.
diff --git a/Cubical/Categories/Constructions/DisplayedCategory.agda b/Cubical/Categories/Constructions/DisplayedCategory.agda
@@ -9,12 +9,11 @@ private
   variable
     ℓC ℓC' ℓP : Level
 
-module _ {ℓC ℓC' : Level} {ℓP : Level} (C : Category ℓC ℓC') where
+module _ {ℓC ℓC' : Level} (C : Category ℓC ℓC') where
 
   open Category
 
-
-  record DisplayedCategory : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-suc ℓP)) where
+  record DisplayedCategory (ℓP : Level) : Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-suc ℓP)) where
     field
       D-ob : C .ob → Type ℓP
       D-Hom_[_,_] : {a b : C .ob} → (f : C [ a , b ])
@@ -43,3 +42,28 @@ module _ {ℓC ℓC' : Level} {ℓP : Level} (C : Category ℓC ℓC') where
                    → PathP (λ i → D-Hom (C .⋆Assoc f g h i) [ x , w ])
                      ((k D-⋆ l) D-⋆ m)
                      (k D-⋆ (l D-⋆ m))
+
+open Category
+open DisplayedCategory
+-- Helpful syntax/notation
+D-hom' : {C : Category ℓC ℓC'}(D : DisplayedCategory C ℓP) → {c c' : C .ob}
+        → (d : D .D-ob c)
+        → (d' : D .D-ob c')
+        → (f : C [ c , c' ])
+        → Type ℓP
+D-hom' D d d' f = D-Hom_[_,_] D f d d'
+
+-- TODO: idea for a better notation PLEASE
+syntax D-hom' D d d' f = D ⊨ f d[ d , d' ]
+
+module _ {C : Category ℓC ℓC'} (D : DisplayedCategory C ℓP) where
+  open DisplayedCategory
+  record Section : Type (ℓ-max (ℓ-max ℓC ℓC') ℓP) where
+    field
+      S-ob  : ∀ c → D .D-ob c
+      S-hom : ∀ {c c'} → (f : C [ c , c' ]) (d : D .D-ob c)(d' : D .D-ob c')
+            → D ⊨ f d[ d , d' ]
+      S-id  : ∀ {c} d → S-hom (C .id {c}) d d ≡ D .D-id
+      S-seq : ∀ {c c' c''} {d d' d''}
+              (f : C [ c , c' ])(f' : C [ c' , c'' ])
+            → S-hom (f ⋆⟨ C ⟩ f') d d'' ≡ D ._D-⋆_ (S-hom f d d') (S-hom f' d' d'')