local elim for Free Cat w/ Terminal, re-org some fibration/terminal s…

…tuff

Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda

@@ -13,12 +13,15 @@ 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
@@ -46,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
@@ -80,9 +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 LiftedTerminalᴰNotation Cᴰ term'ᴰ
+      open LiftedTerminalNotation Cᴰ term'ᴰ
 
       private
         module FC = Category (FreeCatw/Terminal' .fst)
@@ -99,9 +100,6 @@ module _ (Ob : Type ℓg) where
         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
@@ -133,20 +131,23 @@ module _ (Ob : Type ℓg) where
           elim .F-idᴰ = refl
           elim .F-seqᴰ _ _ = refl
 
-    -- module _
-    --   {D : Category ℓD ℓD'}
-    --   {term' : Terminal' D}
-    --   (F : Functor FC D)
-    --   (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ')
-    --   (term'ᴰ : Terminalᴰ Dᴰ term')
-    --   where
-    --   private
-    --     module Dᴰ = Categoryᴰ Dᴰ
-    --   open Terminal'Notation term'
-    --   module _ (ϕ : ∀ o → Dᴰ.ob[ F ⟅ o ⟆ ]) where
-    --     private
-    --       ϕ* : ∀ (o' : Ob') → Dᴰ.ob[ F .F-ob o' ]
-    --       ϕ* = {!!}
+    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)

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/Properties.agda

@@ -31,7 +31,7 @@ open UniversalElement
 module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
          (termC : Terminal' C) (termD : Terminal' D)
          where
-  termWeaken : LiftedTerminalᴰ (weaken C D) termC
+  termWeaken : LiftedTerminal (weaken C D) termC
   termWeaken .vertexᴰ = termD .vertex
   termWeaken .elementᴰ = termD .element
   termWeaken .universalᴰ = termD .universal _

Cubical/Categories/Displayed/Fibration/Base.agda

@@ -23,6 +23,7 @@ private
     ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
 
 open Category
+open Functorᴰ
 
 module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
   private
@@ -156,30 +157,36 @@ module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
         gᴰ⋆π'≡gᴰ⋆π gᴰ =
           R.≡[]-rectify (R.≡[]⋆ refl f'≡f refl (R.reind-filler f'≡f π'))
 
--- package together a fibration and its cleavage, with an explicit base
-ClovenFibration : (C : Category ℓC ℓC') (ℓCᴰ ℓCᴰ' : Level) → Type _
-ClovenFibration C ℓCᴰ ℓCᴰ' = Σ[ Cᴰ ∈ Categoryᴰ C ℓCᴰ ℓCᴰ' ] isFibration Cᴰ
-
 module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
-  (p : ClovenFibration C ℓCᴰ ℓCᴰ')(q : ClovenFibration D ℓDᴰ ℓDᴰ') where
-  module _ {F : Functor C D} (Fᴰ : Functorᴰ F (p .fst) (q .fst)) where
-    open Category
-    open Functorᴰ
-    private
-      module Cᴰ = Categoryᴰ (p .fst)
-
-    -- whether a 1-cell preserves cartesian morphisms
-    isFibered : Type _
-    isFibered =
+  {F : Functor C D}
+  {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+  {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  where
+  private
+    module Cᴰ = Categoryᴰ Cᴰ
+  PreservesCartesianLifts : Functorᴰ F Cᴰ Dᴰ → Type _
+  PreservesCartesianLifts Fᴰ =
       ∀ {c c' : C .ob} (c'ᴰ : Cᴰ.ob[ c' ]) (f : C [ c , c' ]) →
       (f*c'ᴰ : Cᴰ.ob[ c ])(fᴰ : Cᴰ.Hom[ f ][ f*c'ᴰ , c'ᴰ ]) →
-        isCartesianOver (p .fst) c'ᴰ f fᴰ →
-        isCartesianOver (q .fst) (Fᴰ .F-obᴰ c'ᴰ) (F ⟪ f ⟫) (Fᴰ .F-homᴰ fᴰ)
-
-  record FiberedFunctor
-      : Type (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
-      (ℓ-max (ℓ-max ℓCᴰ ℓCᴰ') (ℓ-max ℓDᴰ ℓDᴰ'))) where
-    field
-      base : Functor C D
-      over : Functorᴰ base (p .fst) (q .fst)
-      preserves-cartesian : isFibered over
+        isCartesianOver Cᴰ c'ᴰ f fᴰ →
+        isCartesianOver Dᴰ (Fᴰ .F-obᴰ c'ᴰ) (F ⟪ f ⟫) (Fᴰ .F-homᴰ fᴰ)
+
+-- -- package together a fibration and its cleavage, with an explicit base
+-- ClovenFibration : (C : Category ℓC ℓC') (ℓCᴰ ℓCᴰ' : Level) → Type _
+-- ClovenFibration C ℓCᴰ ℓCᴰ' = Σ[ Cᴰ ∈ Categoryᴰ C ℓCᴰ ℓCᴰ' ] isFibration Cᴰ
+
+-- module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
+--   (p : ClovenFibration C ℓCᴰ ℓCᴰ')(q : ClovenFibration D ℓDᴰ ℓDᴰ') where
+--   module _ {F : Functor C D} (Fᴰ : Functorᴰ F (p .fst) (q .fst)) where
+--     open Category
+--     open Functorᴰ
+--     private
+--       module Cᴰ = Categoryᴰ (p .fst)
+
+--   record FiberedFunctor
+--       : Type (ℓ-max (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD'))
+--       (ℓ-max (ℓ-max ℓCᴰ ℓCᴰ') (ℓ-max ℓDᴰ ℓDᴰ'))) where
+--     field
+--       base : Functor C D
+--       over : Functorᴰ base (p .fst) (q .fst)
+--       preserves-cartesian : PreservesCartesianLifts (p .snd) (q .snd) over

Cubical/Categories/Displayed/Fibration/Properties.agda

@@ -8,10 +8,12 @@ open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor.Base
+open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Limits.Terminal.More
 open import Cubical.Categories.Presheaf.Representable
 open import Cubical.Categories.Displayed.Fibration.Base
 open import Cubical.Categories.Displayed.Instances.Terminal
+open import Cubical.Categories.Displayed.Instances.Terminal.More
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Properties
@@ -25,100 +27,7 @@ private
 
 open Category
 
-module _ {C : Category ℓC ℓC'} where
-  open CartesianOver
-  open FiberedFunctor
-
-  isFibC/C : isFibration (Unitᴰ C)
-  isFibC/C _ = CartesianOver→CartesianLift (Unitᴰ C) ue
-    where
-    ue : CartesianOver (Unitᴰ C) _ _
-    ue .f*cᴰ' = tt
-    ue .π = tt
-    ue .isCartesian _ _ _ =
-      uniqueExists _ (isPropUnit _ _) (λ _ → isSetUnit _ _)
-      λ _ _ → isPropUnit _ _
-
-  -- terminal fibration over C, ie the identity fibration
-  TerminalFib : ClovenFibration C _ _
-  TerminalFib = (Unitᴰ C , isFibC/C)
-
-  module _ (p : ClovenFibration C ℓCᴰ ℓCᴰ') where
-    open Functorᴰ
-
-    !ₚ : FiberedFunctor p TerminalFib
-    !ₚ .base = Id
-    !ₚ .over .F-obᴰ _ = tt
-    !ₚ .over .F-homᴰ _ = tt
-    !ₚ .over .F-idᴰ = refl
-    !ₚ .over .F-seqᴰ _ _ = refl
-    !ₚ .preserves-cartesian _ _ _ _ _ _ _ _ =
-        uniqueExists _ (isPropUnit _ _)
-        (λ _ → isSetUnit _ _) λ _ _ → isPropUnit _ _
-
-    -- Some relevant lemmas:
-    -- Jacobs 1.8.8
-    -- Hermida 1.4.1
-    -- Hermida 3.3.3.i: VerticalRightAdjointᴰ s are automatically fibered?
-    -- Hermida 3.3.6
-    -- In Jacobs too
-
-    -- possible alternative definition
-    VerticalTerminalsᴰ' : Type _
-    VerticalTerminalsᴰ' = VerticalRightAdjointᴰ (!ₚ .over)
-
--- This makes sense for any displayed category,
--- but is traditionally used for fibrations
 module _ {C : Category ℓC ℓC'} (Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ') where
-
-  VerticalTerminalsᴰ : Type _
-  VerticalTerminalsᴰ = (c : C .ob) → VerticalTerminalAtᴰ Cᴰ c
-
-  module _ (term : Terminal' C) where
-
-    open VerticalTerminalAtᴰNotation Cᴰ
-    open UniversalElementᴰ
-    open UniversalElement
-    private module Cᴰ = Categoryᴰ Cᴰ
-
-    Verticalᴰ/𝟙 = VerticalTerminalAtᴰ Cᴰ (term .vertex)
-
-    Verticalᴰ/𝟙→LiftedTermᴰ : Verticalᴰ/𝟙 → LiftedTerminalᴰ Cᴰ term
-    Verticalᴰ/𝟙→LiftedTermᴰ 1ᴰ/1 .vertexᴰ = 1ᴰ/1 .vertexᴰ
-    Verticalᴰ/𝟙→LiftedTermᴰ _ .elementᴰ = tt
-    Verticalᴰ/𝟙→LiftedTermᴰ 1ᴰ/1 .universalᴰ  {xᴰ = xᴰ} {f = f} .equiv-proof _ =
-      uniqueExists (!tᴰ (term .vertex) 1ᴰ/1 f xᴰ) refl
-      (λ _ p q →
-        LiftedTerminalᴰSpec Cᴰ .Functorᴰ.F-obᴰ xᴰ
-        (TerminalPresheaf {C = C} .Functor.F-hom f (term .element))
-          .snd tt tt p q)
-        λ fᴰ' _ → !tᴰ-unique (term .vertex) 1ᴰ/1 f xᴰ .snd fᴰ'
-
-    -- convenience
-    AllVertical→Vertical/𝟙 : VerticalTerminalsᴰ → Verticalᴰ/𝟙
-    AllVertical→Vertical/𝟙 vt = vt (term .vertex)
-
-    -- convenience
-    AllVertical→LiftedTermᴰ : VerticalTerminalsᴰ → LiftedTerminalᴰ Cᴰ term
-    AllVertical→LiftedTermᴰ vt =
-      Verticalᴰ/𝟙→LiftedTermᴰ (AllVertical→Vertical/𝟙 vt)
-
-module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
-  (F : Functor C D)
-  (Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ')
-  (vt : VerticalTerminalsᴰ Dᴰ) where
-  open UniversalElementᴰ
-  open CartesianOver
-
-  -- (this is not just an eta expansion)
-  reind-VerticalTerminalsᴰ : VerticalTerminalsᴰ (reindex Dᴰ F)
-  reind-VerticalTerminalsᴰ c .vertexᴰ = vt (F ⟅ c ⟆) .vertexᴰ
-  reind-VerticalTerminalsᴰ c .elementᴰ = vt (F ⟅ c ⟆) .elementᴰ
-  reind-VerticalTerminalsᴰ c .universalᴰ = vt (F ⟅ c ⟆) .universalᴰ
-
-  module _ (term' : Terminal' C) where
-    -- TODO: this name should be for the "end-to-end" function that reindexes
-    -- the lifted structure of a fibration, by reindexing the vertical structure
-    reind-LiftedTermᴰ : LiftedTerminalᴰ (reindex Dᴰ F) term'
-    reind-LiftedTermᴰ = Verticalᴰ/𝟙→LiftedTermᴰ (reindex Dᴰ F) term'
-      (AllVertical→Vertical/𝟙 (reindex Dᴰ F) term' reind-VerticalTerminalsᴰ)
+  -- alternative definition
+  VerticalTerminals' : Type _
+  VerticalTerminals' = VerticalRightAdjointᴰ (introF {Cᴰ = Cᴰ} Id)

Cubical/Categories/Displayed/Instances/Sets/Properties.agda

@@ -43,15 +43,15 @@ isFibrationSet : isFibration (SETᴰ ℓ ℓ')
 isFibrationSet dᴰ = CartesianOver→CartesianLift (SETᴰ _ _)
   (AllCartesianOversSETᴰ _ _)
 
-VerticalTerminalsᴰSETᴰ : VerticalTerminalsᴰ (SETᴰ ℓ ℓ')
-VerticalTerminalsᴰSETᴰ dᴰ .vertexᴰ _ = Unit* , isSetUnit*
-VerticalTerminalsᴰSETᴰ dᴰ .elementᴰ = tt
-VerticalTerminalsᴰSETᴰ dᴰ .universalᴰ .equiv-proof _ = uniqueExists
+VerticalTerminalsSETᴰ : VerticalTerminals (SETᴰ ℓ ℓ')
+VerticalTerminalsSETᴰ dᴰ .vertexᴰ _ = Unit* , isSetUnit*
+VerticalTerminalsSETᴰ dᴰ .elementᴰ = tt
+VerticalTerminalsSETᴰ dᴰ .universalᴰ .equiv-proof _ = uniqueExists
   (λ _ _ → tt*)
   (isPropUnit tt tt)
   (λ _ p q → isSetUnit tt tt p q)
   (λ _ _ → funExt λ _ → funExt λ _ → refl)
 
-LiftedTerminalᴰSETᴰ : ∀{ℓ ℓ'} → LiftedTerminalᴰ (SETᴰ ℓ ℓ') terminal'SET
-LiftedTerminalᴰSETᴰ {ℓ} {ℓ'} =
-  AllVertical→LiftedTermᴰ (SETᴰ ℓ ℓ') terminal'SET VerticalTerminalsᴰSETᴰ
+LiftedTerminalSETᴰ : ∀{ℓ ℓ'} → LiftedTerminal (SETᴰ ℓ ℓ') terminal'SET
+LiftedTerminalSETᴰ {ℓ} {ℓ'} =
+  Vertical/𝟙→LiftedTerm _ (VerticalTerminalsSETᴰ _)

Cubical/Categories/Displayed/Instances/Terminal/More.agda

@@ -45,3 +45,12 @@ module _ {C : Category ℓC ℓC'}
   recᴰ s .F-idᴰ      = s .F-idᴰ
   recᴰ s .F-seqᴰ _ _ = s .F-seqᴰ _ _
 
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'}
+         (F : Functor C D) where
+  introF : Functorᴰ F Cᴰ (Unitᴰ D)
+  introF .F-obᴰ = λ _ → tt
+  introF .F-homᴰ = λ _ → tt
+  introF .F-idᴰ = refl
+  introF .F-seqᴰ _ _ = refl