update gluing with terminal objects to new defns

maxsnew · Dec 5, 2024 · 31e9bae · 31e9bae
1 parent fb296d3
commit 31e9bae
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 19 deletions.
diff --git a/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda b/Cubical/Categories/Constructions/Free/CategoryWithTerminal.agda
@@ -21,6 +21,7 @@ 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.Base
+open import Cubical.Categories.Displayed.Constructions.Reindex.Limits as Reindex
 open import Cubical.Categories.Displayed.Constructions.Reindex.Properties
 open import Cubical.Categories.Displayed.Reasoning
 
@@ -127,23 +128,23 @@ module _ (Ob : Type ℓg) where
           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'}
+      (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 _ (Vertical/𝟙→LiftedTerm _ (preservesVerticalTerminal _ term'ᴰ)) ϕ ψ)
 
     module _ (D : Category ℓD ℓD')
              (term' : Terminal' D)

diff --git a/Gluing/Terminal.agda b/Gluing/Terminal.agda
@@ -20,7 +20,7 @@ open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Instances.Sets.Base
-open import Cubical.Categories.Displayed.Instances.Sets.Properties
+open import Cubical.Categories.Displayed.Instances.Sets.Properties as SETᴰ
 open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.Sets.Properties
 
@@ -113,7 +113,7 @@ canonicity = λ exp → fixup (Canonicalize .F-homᴰ exp _ _)
 
   Canonicalize : Section pts (SETᴰ _ _)
   Canonicalize = elimLocal _ _ _ _
-    (VerticalTerminalsSETᴰ _)
+    (SETᴰ.hasVerticalTerminals _)
     (λ { e _ → Empty.⊥* , isProp→isSet isProp⊥*
        ; b exp → CanonicalForm exp , isSetCanonicalForm
        })