(Displayed) Category Theory: Sections of displayed categories, Free C…

…ategory 3.0 and UMPs are Props (#1149)

* univalence of the cat of elements, universal props on univalent cats are Props

* facts about composition of functors + whiskering of isomorphisms

* Sections of displayed categories

* displayed category of Paths between objects

* Yet another free category

Cubical/Categories/Constructions/BinProduct.agda

@@ -65,6 +65,12 @@ module _ where
   _×F_ : Functor A C → Functor B D → Functor (A ×C B) (C ×C D)
   _×F_ {A = A} {B = B} G H = G ∘F Fst A B ,F H ∘F Snd A B
 
+Δ : ∀ (C : Category ℓC ℓC') → Functor C (C ×C C)
+Δ C = Id ,F Id
+
+Sym : {C : Category ℓC ℓC'}{D : Category ℓD ℓD'} → Functor (C ×C D) (D ×C C)
+Sym {C = C}{D = D} = Snd C D ,F Fst C D
+
 -- Some useful functors
 module _ (C : Category ℓC ℓC')
          (D : Category ℓD ℓD') where

Cubical/Categories/Constructions/DisplayOverTerminal.agda

@@ -0,0 +1,31 @@
+{-
+  A category displayed over the terminal category is isomorphic to
+  just a category.
+-}
+
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.DisplayOverTerminal where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Unit
+open import Cubical.Categories.Category
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Instances.Terminal
+
+
+private
+  variable
+    ℓC ℓ'C ℓD ℓ'D ℓCᴰ ℓ'Cᴰ ℓDᴰ ℓ'Dᴰ : Level
+module _ {ℓ* : Level} (Cᴰ : Categoryᴰ (TerminalCategory {ℓ*}) ℓCᴰ ℓ'Cᴰ) where
+  open Categoryᴰ Cᴰ
+  open Category
+
+  DispOverTerminal→Category : Category ℓCᴰ ℓ'Cᴰ
+  DispOverTerminal→Category .ob = ob[ tt* ]
+  DispOverTerminal→Category .Hom[_,_] = Hom[ refl ][_,_]
+  DispOverTerminal→Category .id = idᴰ
+  DispOverTerminal→Category ._⋆_ = _⋆ᴰ_
+  DispOverTerminal→Category .⋆IdL = ⋆IdLᴰ
+  DispOverTerminal→Category .⋆IdR = ⋆IdRᴰ
+  DispOverTerminal→Category .⋆Assoc = ⋆Assocᴰ
+  DispOverTerminal→Category .isSetHom = isSetHomᴰ

Cubical/Categories/Constructions/Elements.agda

@@ -1,8 +1,9 @@
 {-# OPTIONS --safe #-}
 
--- The Category of Elements
+-- The category of elements of a functor to Set
 
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Path
@@ -86,6 +87,31 @@ module Covariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     F-id (ForgetElements F) = refl
     F-seq (ForgetElements F) _ _ = refl
 
+    module _ (isUnivC : isUnivalent C) {ℓS} (F : Functor C (SET ℓS)) where
+      open isUnivalent
+      isUnivalent∫ : isUnivalent (∫ F)
+      isUnivalent∫ .univ (c , f) (c' , f') = isIsoToIsEquiv
+        ( isoToPath∫
+        , (λ f≅f' → CatIso≡ _ _
+            (Σ≡Prop (λ _ → (F ⟅ _ ⟆) .snd _ _)
+              (cong fst
+              (secEq (univEquiv isUnivC _ _) (F-Iso {F = ForgetElements F} f≅f')))))
+        , λ f≡f' → ΣSquareSet (λ x → snd (F ⟅ x ⟆))
+          ( cong (CatIsoToPath isUnivC) (F-pathToIso {F = ForgetElements F} f≡f')
+          ∙ retEq (univEquiv isUnivC _ _) (cong fst f≡f'))) where
+
+        isoToPath∫ : ∀ {c c' f f'}
+                   → CatIso (∫ F) (c , f) (c' , f')
+                   → (c , f) ≡ (c' , f')
+        isoToPath∫ {f = f} f≅f' = ΣPathP
+          ( CatIsoToPath isUnivC (F-Iso {F = ForgetElements F} f≅f')
+          , toPathP ( (λ j → transport (λ i → fst
+                      (F-isoToPath isUnivC isUnivalentSET F
+                        (F-Iso {F = ForgetElements F} f≅f') (~ j) i)) f)
+                    ∙ univSetβ (F-Iso {F = F ∘F ForgetElements F} f≅f') f
+                    ∙ f≅f' .fst .snd))
+
+
 module Contravariant {ℓ ℓ'} {C : Category ℓ ℓ'} where
     open Covariant {C = C ^op}
 

Cubical/Categories/Constructions/Free/Category/Quiver.agda

@@ -0,0 +1,162 @@
+-- Free category generated from base objects and generators
+
+-- This time using a "quiver" as the presentation of the generators,
+-- which is better in some applications
+{-# OPTIONS --safe #-}
+
+module Cubical.Categories.Constructions.Free.Category.Quiver where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Sigma
+open import Cubical.Data.Quiver.Base as Quiver
+open import Cubical.Data.Graph.Base as Graph
+open import Cubical.Data.Graph.Displayed as Graph hiding (Section)
+
+open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Constructions.BinProduct as BP
+open import Cubical.Categories.UnderlyingGraph hiding (Interp)
+open import Cubical.Categories.Displayed.Base
+open import Cubical.Categories.Displayed.Instances.Path
+open import Cubical.Categories.Displayed.Constructions.Reindex.Base as Reindex
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
+
+open import Cubical.Categories.Displayed.Section.Base as Cat
+
+private
+  variable
+    ℓc ℓc' ℓd ℓd' ℓg ℓg' ℓh ℓh' ℓj ℓ : Level
+    ℓC ℓC' ℓCᴰ ℓCᴰ' : Level
+
+open Category
+open Functor
+open QuiverOver
+
+module _ (Q : Quiver ℓg ℓg') where
+  data Exp : Q .fst → Q .fst → Type (ℓ-max ℓg ℓg') where
+    ↑_   : ∀ g → Exp (Q .snd .dom g) (Q .snd .cod g)
+    idₑ  : ∀ {A} → Exp A A
+    _⋆ₑ_ : ∀ {A B C} → (e : Exp A B) → (e' : Exp B C) → Exp A C
+    ⋆ₑIdL : ∀ {A B} (e : Exp A B) → idₑ ⋆ₑ e ≡ e
+    ⋆ₑIdR : ∀ {A B} (e : Exp A B) → e ⋆ₑ idₑ ≡ e
+    ⋆ₑAssoc : ∀ {A B C D} (e : Exp A B)(f : Exp B C)(g : Exp C D)
+            → (e ⋆ₑ f) ⋆ₑ g ≡ e ⋆ₑ (f ⋆ₑ g)
+    isSetExp : ∀ {A B} → isSet (Exp A B)
+
+  FreeCat : Category _ _
+  FreeCat .ob = Q .fst
+  FreeCat .Hom[_,_] = Exp
+  FreeCat .id = idₑ
+  FreeCat ._⋆_ = _⋆ₑ_
+  FreeCat .⋆IdL = ⋆ₑIdL
+  FreeCat .⋆IdR = ⋆ₑIdR
+  FreeCat .⋆Assoc = ⋆ₑAssoc
+  FreeCat .isSetHom = isSetExp
+
+  Interp : (𝓒 : Category ℓc ℓc') → Type (ℓ-max (ℓ-max (ℓ-max ℓg ℓg') ℓc) ℓc')
+  Interp 𝓒 = HetQG Q (Cat→Graph 𝓒)
+
+  η : Interp FreeCat
+  η HetQG.$g x = x
+  η HetQG.<$g> e = ↑ e
+
+  module _ {C : Category ℓC ℓC'}
+           (ı : Interp C)
+           (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
+    Interpᴰ : Type _
+    Interpᴰ = HetSection ı (Categoryᴰ→Graphᴰ Cᴰ)
+
+  -- the eliminator constructs a *global* section. Use reindexing if
+  -- you want a local section
+  module _ (Cᴰ : Categoryᴰ FreeCat ℓCᴰ ℓCᴰ')
+           (ıᴰ : Interpᴰ η Cᴰ)
+           where
+    open HetSection
+    open Section
+    private module Cᴰ = Categoryᴰ Cᴰ
+
+    elim-F-homᴰ : ∀ {d d'} → (f : FreeCat .Hom[_,_] d d') →
+      Cᴰ.Hom[ f ][ ıᴰ $gᴰ d , (ıᴰ $gᴰ d') ]
+    elim-F-homᴰ (↑ g) = ıᴰ <$g>ᴰ g
+    elim-F-homᴰ idₑ = Cᴰ.idᴰ
+    elim-F-homᴰ (f ⋆ₑ g) = elim-F-homᴰ f Cᴰ.⋆ᴰ elim-F-homᴰ g
+    elim-F-homᴰ (⋆ₑIdL f i) = Cᴰ.⋆IdLᴰ (elim-F-homᴰ f) i
+    elim-F-homᴰ (⋆ₑIdR f i) = Cᴰ.⋆IdRᴰ (elim-F-homᴰ f) i
+    elim-F-homᴰ (⋆ₑAssoc f f₁ f₂ i) =
+      Cᴰ.⋆Assocᴰ (elim-F-homᴰ f) (elim-F-homᴰ f₁) (elim-F-homᴰ f₂) i
+    elim-F-homᴰ (isSetExp f g p q i j) = isOfHLevel→isOfHLevelDep 2
+      (λ x → Cᴰ.isSetHomᴰ)
+      (elim-F-homᴰ f) (elim-F-homᴰ g)
+      (cong elim-F-homᴰ p) (cong elim-F-homᴰ q)
+      (isSetExp f g p q)
+      i j
+
+    elim : GlobalSection Cᴰ
+    elim .F-obᴰ = ıᴰ $gᴰ_
+    elim .F-homᴰ = elim-F-homᴰ
+    elim .F-idᴰ = refl
+    elim .F-seqᴰ _ _ = refl
+
+  -- The elimination principle for global sections implies an
+  -- elimination principle for local sections, this requires reindex
+  -- so caveat utilitor
+  module _ {C : Category ℓC ℓC'}
+           (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ')
+           (F : Functor FreeCat C)
+           (ıᴰ : Interpᴰ (compGrHomHetQG (Functor→GraphHom F) η) Cᴰ)
+           where
+    private
+      open HetSection
+      F*Cᴰ = Reindex.reindex Cᴰ F
+      ıᴰ' : Interpᴰ η F*Cᴰ
+      ıᴰ' ._$gᴰ_ = ıᴰ $gᴰ_
+      ıᴰ' ._<$g>ᴰ_ = ıᴰ <$g>ᴰ_
+
+    elimLocal : Section F Cᴰ
+    elimLocal = GlobalSectionReindex→Section Cᴰ F (elim F*Cᴰ ıᴰ')
+
+  -- Elimination principle implies the recursion principle, which
+  -- allows for non-dependent functors to be defined
+  module _ {C : Category ℓC ℓC'} (ı : Interp C) where
+    open HetQG
+    private
+      ıᴰ : Interpᴰ η (weaken FreeCat C)
+      ıᴰ .HetSection._$gᴰ_ = ı .HetQG._$g_
+      ıᴰ .HetSection._<$g>ᴰ_ = ı .HetQG._<$g>_
+
+    rec : Functor FreeCat C
+    rec = Wk.introS⁻ (elim (weaken FreeCat C) ıᴰ)
+
+  -- Elimination principle also implies the uniqueness principle,
+  -- i.e., η law for sections/functors out of the free category
+  -- this version is for functors
+  module _
+    {C : Category ℓC ℓC'}
+    (F G : Functor FreeCat C)
+    (agree-on-gen :
+      -- todo: some notation would simplify this considerably
+      Interpᴰ (compGrHomHetQG (Functor→GraphHom (F BP.,F G)) η) (PathC C))
+    where
+    FreeCatFunctor≡ : F ≡ G
+    FreeCatFunctor≡ = PathReflection (elimLocal (PathC C) _ agree-on-gen)
+
+  -- TODO: add analogous principle for Sections using PathCᴰ
+-- -- co-unit of the 2-adjunction
+module _ {𝓒 : Category ℓc ℓc'} where
+  private
+    Exp⟨𝓒⟩ = FreeCat (Cat→Quiver 𝓒)
+  ε : Functor Exp⟨𝓒⟩ 𝓒
+  ε = rec (Cat→Quiver 𝓒)
+    (record { _$g_ = λ z → z ; _<$g>_ = λ e → e .snd .snd })
+
+  ε-reasoning : {𝓓 : Category ℓd ℓd'}
+            → (𝓕 : Functor 𝓒 𝓓)
+            → 𝓕 ∘F ε ≡ rec (Cat→Quiver 𝓒)
+      (record { _$g_ = 𝓕 .F-ob ; _<$g>_ = λ e → 𝓕 .F-hom (e .snd .snd) })
+  ε-reasoning 𝓕 = FreeCatFunctor≡ _ _ _
+    (record { _$gᴰ_ = λ _ → refl ; _<$g>ᴰ_ = λ _ → refl })

Cubical/Categories/Constructions/Opposite.agda

@@ -0,0 +1,40 @@
+{-# OPTIONS --safe #-}
+module Cubical.Categories.Constructions.Opposite where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor.Base
+
+open import Cubical.Categories.Isomorphism
+
+private
+  variable
+    ℓC ℓC' ℓD ℓD' : Level
+
+open Category
+open Functor
+open isUnivalent
+
+module _ {C : Category ℓC ℓC'} (isUnivC : isUnivalent C) where
+  op-Iso-pathToIso : ∀ {x y : C .ob} (p : x ≡ y)
+                   → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p
+  op-Iso-pathToIso =
+    J (λ y p → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p)
+      (CatIso≡ _ _ refl)
+
+  op-Iso-pathToIso' : ∀ {x y : C .ob} (p : x ≡ y)
+                   → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p
+  op-Iso-pathToIso' =
+    J (λ y p → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p)
+      (CatIso≡ _ _ refl)
+
+  isUnivalentOp : isUnivalent (C ^op)
+  isUnivalentOp .univ x y = isIsoToIsEquiv
+    ( (λ f^op → CatIsoToPath isUnivC (op-Iso f^op))
+    , (λ f^op → CatIso≡ _ _
+        (cong fst
+        (cong op-Iso ((secEq (univEquiv isUnivC _ _) (op-Iso f^op))))))
+    , λ p → cong (CatIsoToPath isUnivC) (op-Iso-pathToIso' p)
+        ∙ retEq (univEquiv isUnivC _ _) p)

Cubical/Categories/Constructions/TotalCategory.agda

@@ -1,74 +1,5 @@
 {-# OPTIONS --safe #-}
 module Cubical.Categories.Constructions.TotalCategory where
 
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.HLevels
-
-open import Cubical.Data.Sigma
-
-open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Instances.Terminal
-
-private
-  variable
-    ℓC ℓC' ℓD ℓD' ℓE ℓE' ℓCᴰ ℓCᴰ' ℓDᴰ ℓDᴰ' ℓEᴰ ℓEᴰ' : Level
-
--- Total category of a displayed category
-module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
-
-  open Category
-  open Categoryᴰ Cᴰ
-  private
-    module C = Category C
-
-  ∫C : Category (ℓ-max ℓC ℓCᴰ) (ℓ-max ℓC' ℓCᴰ')
-  ∫C .ob = Σ _ ob[_]
-  ∫C .Hom[_,_] (_ , xᴰ) (_ , yᴰ) = Σ _ Hom[_][ xᴰ , yᴰ ]
-  ∫C .id = _ , idᴰ
-  ∫C ._⋆_ (_ , fᴰ) (_ , gᴰ) = _ , fᴰ ⋆ᴰ gᴰ
-  ∫C .⋆IdL _ = ΣPathP (_ , ⋆IdLᴰ _)
-  ∫C .⋆IdR _ = ΣPathP (_ , ⋆IdRᴰ _)
-  ∫C .⋆Assoc _ _ _ = ΣPathP (_ , ⋆Assocᴰ _ _ _)
-  ∫C .isSetHom = isSetΣ C.isSetHom (λ _ → isSetHomᴰ)
-
--- Total functor of a displayed functor
-module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
-  {F : Functor C D} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
-  (Fᴰ : Functorᴰ F Cᴰ Dᴰ)
-  where
-
-  open Functor
-  private
-    module Fᴰ = Functorᴰ Fᴰ
-
-  ∫F : Functor (∫C Cᴰ) (∫C Dᴰ)
-  ∫F .F-ob (x , xᴰ) = _ , Fᴰ.F-obᴰ xᴰ
-  ∫F .F-hom (_ , fᴰ) = _ , Fᴰ.F-homᴰ fᴰ
-  ∫F .F-id = ΣPathP (_ , Fᴰ.F-idᴰ)
-  ∫F .F-seq _ _ = ΣPathP (_ , (Fᴰ.F-seqᴰ _ _))
-
--- Projections out of the total category
-module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
-  open Functor
-  open Functorᴰ
-
-  Fst : Functor (∫C Cᴰ) C
-  Fst .F-ob = fst
-  Fst .F-hom = fst
-  Fst .F-id = refl
-  Fst .F-seq =
-    λ f g → cong {x = f ⋆⟨ ∫C Cᴰ ⟩ g} fst refl
-
-  -- Functor into the total category
-  module _ {D : Category ℓD ℓD'}
-           (F : Functor D C)
-           (Fᴰ : Functorᴰ F (Unitᴰ D) Cᴰ)
-           where
-    intro : Functor D (∫C Cᴰ)
-    intro .F-ob d = F ⟅ d ⟆ , Fᴰ .F-obᴰ _
-    intro .F-hom f = (F ⟪ f ⟫) , (Fᴰ .F-homᴰ _)
-    intro .F-id = ΣPathP (F .F-id , Fᴰ .F-idᴰ)
-    intro .F-seq f g = ΣPathP (F .F-seq f g , Fᴰ .F-seqᴰ _ _)
+open import Cubical.Categories.Constructions.TotalCategory.Base public
+open import Cubical.Categories.Constructions.TotalCategory.Properties public