Gluing for Free cat with terminal objects

Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda

@@ -1,24 +1,36 @@
+{-# OPTIONS --safe #-}
 -- Free category with a terminal object, over a Quiver
 module Cubical.Categories.Constructions.Free.CategoryWithTerminal where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
 
 open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
 open import Cubical.Categories.Limits.Terminal.More
 open import Cubical.Data.Quiver.Base
-open import Cubical.Data.Sum.Base as Sum hiding (elim)
+open import Cubical.Data.Sum.Base as Sum hiding (elim; rec)
 open import Cubical.Data.Unit
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Presheaf
+open import Cubical.Categories.Displayed.Properties
 open import Cubical.Categories.Displayed.Presheaf
 open import Cubical.Categories.Displayed.Limits.Terminal
 open import Cubical.Foundations.Equiv
 open import Cubical.Data.Sigma.Properties
 open import Cubical.Categories.Displayed.Section.Base
+open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
+open import Cubical.Categories.Displayed.Constructions.Reindex
+open import Cubical.Categories.Displayed.Constructions.Reindex.Properties
+open import Cubical.Categories.Displayed.Reasoning
 
 private
   variable
-    ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' : Level
+    ℓg ℓg' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
+
+open Section
+open Functor
+open UniversalElementᴰ
 
 CategoryWithTerminal' : (ℓC ℓC' : Level) → Type _
 CategoryWithTerminal' ℓC ℓC' = Σ[ C ∈ Category ℓC ℓC' ] Terminal' C
@@ -37,8 +49,6 @@ module _ (Ob : Type ℓg) where
     open QuiverOver
     open UniversalElement
 
-    -- copied from Categories.Constructions.Free.Category.Quiver
-    -- and suitably modified
     data Exp : Ob' → Ob' → Type (ℓ-max ℓg ℓg') where
       ↑_   : ∀ g → Exp (Q .dom g) (Q .cod g)
       idₑ  : ∀ {A} → Exp A A
@@ -71,13 +81,9 @@ module _ (Ob : Type ℓg) where
     FreeCatw/Terminal' = (FC , FCTerminal')
 
     module _ (Cᴰ : Categoryᴰ (FreeCatw/Terminal' .fst) ℓCᴰ ℓCᴰ')
-      (term'ᴰ : LiftedTerminalᴰ Cᴰ (FreeCatw/Terminal' .snd)) where
+      (term'ᴰ : LiftedTerminal Cᴰ (FreeCatw/Terminal' .snd)) where
 
-      open import Cubical.Foundations.HLevels
-      open import Cubical.Categories.Displayed.Reasoning
-      open Section
-      open UniversalElementᴰ
-      open LiftedTerminalᴰNotation Cᴰ term'ᴰ
+      open LiftedTerminalNotation Cᴰ term'ᴰ
 
       private
         module FC = Category (FreeCatw/Terminal' .fst)
@@ -86,16 +92,14 @@ module _ (Ob : Type ℓg) where
       -- given an interpretation of atomic objects
       module _ (ϕ : (v : Ob) → Cᴰ.ob[ inl v ]) where
         -- extend it to all objects
-        ϕ* : (v : Ob') → Cᴰ.ob[ v ]
-        ϕ* = Sum.elim (λ a → ϕ a) (λ b → term'ᴰ .vertexᴰ)
+        private
+          ϕ* : (v : Ob') → Cᴰ.ob[ v ]
+          ϕ* = Sum.elim (λ a → ϕ a) (λ b → term'ᴰ .vertexᴰ)
 
         -- and given an interpretation of atomic morphisms
         module _ (ψ : (e : Q .mor) →
           Cᴰ.Hom[ ↑ e ][ ϕ* (Q .dom e) , ϕ* (Q .cod e) ]) where
 
-          -- extend it to all morphisms
-          -- (copied from
-          -- Cubical.Categories.Constructions.Free.Category.Quiver)
           elim-F-homᴰ : ∀ {d d'} → (f : FC.Hom[ d , d' ]) →
             Cᴰ.Hom[ f ][ ϕ* d , ϕ* d' ]
           elim-F-homᴰ (↑ g) = ψ g
@@ -126,3 +130,34 @@ module _ (Ob : Type ℓg) where
           elim .F-homᴰ = elim-F-homᴰ
           elim .F-idᴰ = refl
           elim .F-seqᴰ _ _ = refl
+
+    module _
+      {D : Category ℓD ℓD'}
+      (F : Functor FC D)
+      (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ')
+      (term'ᴰ : VerticalTerminalAt Dᴰ (F ⟅ inr _ ⟆))
+      where
+      private
+        module Dᴰ = Categoryᴰ Dᴰ
+        open VerticalTerminalAtNotation _ _ term'ᴰ
+      module _ (ϕ : ∀ o → Dᴰ.ob[ F ⟅ inl o ⟆ ]) where
+        private
+          ϕ* : ∀ v → Dᴰ.ob[ F ⟅ v ⟆ ]
+          ϕ* = Sum.elim ϕ λ _ → 1ᴰ
+        module _ (ψ : ∀ e → Dᴰ.Hom[ F ⟪ ↑ e ⟫ ][ ϕ* _ , ϕ* _ ]) where
+          elimLocal : Section F Dᴰ
+          elimLocal = GlobalSectionReindex→Section _ _
+            (elim _ (LiftedTerminalReindex term'ᴰ) ϕ ψ)
+
+    module _ (D : Category ℓD ℓD')
+             (term' : Terminal' D)
+             (ϕ : Ob → D .ob)
+             where
+      private
+        open Terminal'Notation term'
+        ϕ* : Ob' → D .ob
+        ϕ* = Sum.elim (λ a → ϕ a) λ _ → 𝟙
+
+      module _ (ψ : ∀ e → D [ ϕ* (Q .dom e) , ϕ* (Q .cod e) ]) where
+        rec : Functor FC D
+        rec = Wk.introS⁻ (elim (weaken FC D) (termWeaken _ term') ϕ ψ)

Cubical/Categories/Displayed/Constructions/BinProduct/More.agda

@@ -26,6 +26,7 @@ open import Cubical.Categories.Constructions.TotalCategory.More
 open import Cubical.Categories.Displayed.Constructions.TotalCategory
 open import Cubical.Categories.Displayed.Instances.Terminal as Unitᴰ
 open import Cubical.Categories.Displayed.Instances.Terminal.More as Unitᴰ
+  hiding (introF)
 
 private
   variable

Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda

@@ -8,21 +8,27 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Limits.Terminal.More
 open import Cubical.Categories.Functor
+open import Cubical.Categories.Presheaf
 
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Properties
+open import Cubical.Categories.Displayed.Limits.Terminal
 import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Displayed.Fibration.Base
+open import Cubical.Categories.Displayed.Presheaf
 
 private
   variable
     ℓB ℓB' ℓBᴰ ℓBᴰ' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
 
 open Category
 open Functor
+open UniversalElement
+open UniversalElementᴰ
+open CartesianOver
 
-{- -}
 module _
   {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
   (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ') (F : Functor C D)
@@ -40,7 +46,6 @@ module _
     {c : C .ob}{c' : C .ob}
     {dᴰ' : Dᴰ.ob[ F ⟅ c' ⟆ ]}{f : C [ c , c' ]}
     where
-    open CartesianOver
     reflectsCartesianOvers
       : CartesianOver Dᴰ dᴰ' (F ⟪ f ⟫)
       → CartesianOver F*Dᴰ dᴰ' f
@@ -72,3 +77,30 @@ module _
             (R.reind-filler (sym (F .F-seq _ _)) _)
             gᴰ-commutes)
             (R.reind-filler (F .F-seq g f) gfᴰ)))))
+
+module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+  {F : Functor C D}
+  {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  where
+
+  reindReflectsVerticalTerminal :
+    ∀ c → VerticalTerminalAt Dᴰ (F ⟅ c ⟆)
+    → VerticalTerminalAt (reindex Dᴰ F) c
+  reindReflectsVerticalTerminal c 𝟙ᴰ .vertexᴰ = 𝟙ᴰ .vertexᴰ
+  reindReflectsVerticalTerminal c 𝟙ᴰ .elementᴰ = 𝟙ᴰ .elementᴰ
+  reindReflectsVerticalTerminal c 𝟙ᴰ .universalᴰ = 𝟙ᴰ .universalᴰ
+
+  VerticalTerminalsReindex :
+    VerticalTerminals Dᴰ
+    → VerticalTerminals (reindex Dᴰ F)
+  VerticalTerminalsReindex vta c =
+    reindReflectsVerticalTerminal c (vta (F ⟅ c ⟆))
+
+  module _ {termC : Terminal' C} where
+    open Terminal'Notation termC
+    LiftedTerminalReindex :
+      VerticalTerminalAt Dᴰ (F ⟅ 𝟙 ⟆)
+      → LiftedTerminal (reindex Dᴰ F) termC
+    LiftedTerminalReindex 𝟙ᴰ =
+      Vertical/𝟙→LiftedTerm _
+        (reindReflectsVerticalTerminal (termC .vertex) 𝟙ᴰ)

Cubical/Categories/Displayed/Constructions/Weaken.agda

@@ -1,105 +1,5 @@
-{-
-
-  Weaken a category to be a displayed category.
-
-  Later: weaken a displayed category to depend on fewer parameters?
-
--}
-
 {-# OPTIONS --safe #-}
---
 module Cubical.Categories.Displayed.Constructions.Weaken 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.Section.Base
-open import Cubical.Categories.Displayed.Properties
-open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Constructions.TotalCategory as TC
-  hiding (intro)
-open import Cubical.Categories.Constructions.TotalCategory.More as TC
-
-private
-  variable
-    ℓB ℓB' ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' ℓE ℓE' ℓEᴰ ℓEᴰ' : Level
-
-open Categoryᴰ
-
-module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
-  open Category
-  weaken : Categoryᴰ C ℓD ℓD'
-  weaken .ob[_] x = D .ob
-  weaken .Hom[_][_,_] f d d' = D [ d , d' ]
-  weaken .idᴰ = D .id
-  weaken ._⋆ᴰ_ = D ._⋆_
-  weaken .⋆IdLᴰ = D .⋆IdL
-  weaken .⋆IdRᴰ = D .⋆IdR
-  weaken .⋆Assocᴰ = D .⋆Assoc
-  weaken .isSetHomᴰ = D .isSetHom
-
-  open Functor
-  weakenΠ : Functor (∫C weaken) D
-  weakenΠ .F-ob = snd
-  weakenΠ .F-hom = snd
-  weakenΠ .F-id = refl
-  weakenΠ .F-seq _ _ = refl
-
-module _ {C : Category ℓC ℓC'}
-         {D : Category ℓD ℓD'}
-         {E : Category ℓE ℓE'}
-         (F : Functor E C)
-         (G : Functor E D)
-         where
-  open Category
-  open Functor
-  open Section
-  introS : Section F (weaken C D)
-  introS .F-obᴰ x = G .F-ob x
-  introS .F-homᴰ f = G .F-hom f
-  introS .F-idᴰ = G .F-id
-  introS .F-seqᴰ _ _ = G .F-seq _ _
-
-module _ {C : Category ℓC ℓC'}
-         {D : Category ℓD ℓD'}
-         {E : Category ℓE ℓE'}
-         {Eᴰ : Categoryᴰ E ℓEᴰ ℓEᴰ'}
-         (F : Functor E C)
-         (G : Functor E D)
-         where
-  open Category
-  open Functor
-  open Functorᴰ
-  introF : Functorᴰ F Eᴰ (weaken C D)
-  introF .F-obᴰ {x} _ = G .F-ob x
-  introF .F-homᴰ {x} {y} {f} {xᴰ} {yᴰ} _ = G .F-hom f
-  introF .F-idᴰ = G .F-id
-  introF .F-seqᴰ _ _ = G .F-seq _ _
-
-introS⁻ : {C : Category ℓC ℓC'}
-         {D : Category ℓD ℓD'}
-         {E : Category ℓE ℓE'}
-         {F : Functor E C}
-       → Section F (weaken C D)
-       → Functor E D
-introS⁻ {C = C}{D = D}{F = F} Fᴰ =
-  weakenΠ C D ∘F TC.intro' F Fᴰ
-
--- TODO: introS/introS⁻ is an Iso
-
-module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where
-  open Functor
-  open Functorᴰ
-
-  weakenF : {D : Category ℓD ℓD'} {E : Category ℓE ℓE'} {F : Functor B C}
-          → (G : Functor D E)
-          → Functorᴰ F (weaken B D) (weaken C E)
-  weakenF G .F-obᴰ = G .F-ob
-  weakenF G .F-homᴰ = G .F-hom
-  weakenF G .F-idᴰ = G .F-id
-  weakenF G .F-seqᴰ = G .F-seq
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base public
+open import Cubical.Categories.Displayed.Constructions.Weaken.Properties public