local eliminator and recursor for cartesian category

maxsnew · Jun 20, 2024 · 0849f9f · 0849f9f
1 parent 564e32f
commit 0849f9f
Show file tree

Hide file tree

Showing 11 changed files with 187 additions and 62 deletions.
diff --git a/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda b/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda
@@ -5,11 +5,14 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma hiding (_×_)
+import Cubical.Data.Sigma as Σ
 
 open import
   Cubical.Categories.Constructions.Free.CartesianCategory.ProductQuiver
 open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Functor
 open import Cubical.Categories.Limits.Cartesian.Base
+open import Cubical.Categories.Limits.Terminal.More
 open import Cubical.Categories.Limits.BinProduct
 open import Cubical.Categories.Limits.BinProduct.More
 
@@ -20,16 +23,21 @@ open import Cubical.Categories.Displayed.Limits.Terminal
 open import Cubical.Categories.Displayed.Limits.BinProduct
 open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Presheaf
+open import Cubical.Categories.Displayed.Properties
+open import Cubical.Categories.Displayed.Constructions.Reindex
+open import Cubical.Categories.Displayed.Constructions.Reindex.Properties
+open import Cubical.Categories.Displayed.Fibration.Base
+open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
 
 private
   variable
-    ℓQ ℓCᴰ ℓCᴰ' : Level
+    ℓQ ℓC ℓC' ℓCᴰ ℓCᴰ' ℓD ℓD' ℓDᴰ ℓDᴰ' : Level
 
 module _ (Q : ×Quiver ℓQ) where
   open ProductQuiver
-  open ×QuiverNotation Q
-  data Exp : Ob → Ob → Type ℓQ where
-    ↑ₑ_ : ∀ t → Exp (Dom t) (Cod t)
+  private module Q = ×QuiverNotation Q
+  data Exp : Q.Ob → Q.Ob → Type ℓQ where
+    ↑ₑ_ : ∀ t → Exp (Q.Dom t) (Q.Cod t)
     idₑ : ∀{Γ} → Exp Γ Γ
     _⋆ₑ_ : ∀{Γ Γ' Γ''}(δ : Exp Γ Γ') → (δ' : Exp Γ' Γ'') →  Exp Γ Γ''
     ⋆ₑIdL : ∀{Γ Δ}(δ : Exp Γ Δ) → idₑ ⋆ₑ δ ≡ δ
@@ -49,7 +57,7 @@ module _ (Q : ×Quiver ℓQ) where
 
   open Category
   |FreeCartesianCategory| : Category _ _
-  |FreeCartesianCategory| .ob = Ob
+  |FreeCartesianCategory| .ob = Q.Ob
   |FreeCartesianCategory| .Hom[_,_] = Exp
   |FreeCartesianCategory| .id = idₑ
   |FreeCartesianCategory| ._⋆_ = _⋆ₑ_
@@ -82,51 +90,139 @@ module _ (Q : ×Quiver ℓQ) where
       open LiftedBinProductsNotation bpᴰ
     open UniversalElementᴰ
     module _ (ı-ob : ∀ o → Cᴰ.ob[ ↑ o ]) where
-      private
-        elim-F-ob : ∀ c → Cᴰ.ob[ c ]
-        elim-F-ob (↑ o)     = ı-ob o
-        elim-F-ob ⊤         = 𝟙ᴰ
-        elim-F-ob (c₁ × c₂) = elim-F-ob c₁ ×ᴰ elim-F-ob c₂
+      elim-F-ob : ∀ c → Cᴰ.ob[ c ]
+      elim-F-ob (↑ o)     = ı-ob o
+      elim-F-ob ⊤         = 𝟙ᴰ
+      elim-F-ob (c₁ × c₂) = elim-F-ob c₁ ×ᴰ elim-F-ob c₂
 
       module _ (ı-hom : ∀ e →
-        Cᴰ.Hom[ ↑ₑ e ][ elim-F-ob (Dom e) , elim-F-ob (Cod e) ])
+        Cᴰ.Hom[ ↑ₑ e ][ elim-F-ob (Q.Dom e) , elim-F-ob (Q.Cod e) ])
         where
         open Section
         private
           module R = HomᴰReasoning Cᴰ
 
-          elim-F-hom : ∀ {c c'} (f : |FreeCartesianCategory| [ c , c' ]) →
-            Cᴰ [ f ][ elim-F-ob c , elim-F-ob c' ]
-          elim-F-hom (↑ₑ t) = ı-hom t
-          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 g h i) =
-            Cᴰ.⋆Assocᴰ (elim-F-hom f) (elim-F-hom g) (elim-F-hom h) i
-          elim-F-hom (isSetExp f g p q i j) =
-            isOfHLevel→isOfHLevelDep 2 (λ _ → 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-F-hom !ₑ = !tᴰ _
-          -- TODO: Why does this need rectify?
-          elim-F-hom (⊤η f i) =
-            R.≡[]-rectify {p' = ⊤η f} (𝟙ηᴰ (elim-F-hom f)) i
-          elim-F-hom π₁ = π₁ᴰ
-          elim-F-hom π₂ = π₂ᴰ
-          elim-F-hom ⟨ f₁ , f₂ ⟩ = elim-F-hom f₁ ,pᴰ elim-F-hom f₂
-          elim-F-hom (×β₁ {t = f₁}{t' = f₂} i) =
-            ×β₁ᴰ {f₁ᴰ = elim-F-hom f₁} {f₂ᴰ = elim-F-hom f₂} i
-          elim-F-hom (×β₂ {t = f₁}{t' = f₂} i) =
-            ×β₂ᴰ {f₁ᴰ = elim-F-hom f₁} {f₂ᴰ = elim-F-hom f₂} i
-          -- TODO: Why do we need this rectify too?
-          elim-F-hom (×η {t = f} i) =
-            R.≡[]-rectify {p' = ×η {t = f}} (×ηᴰ {fᴰ = elim-F-hom f}) i
+        elim-F-hom : ∀ {c c'} (f : |FreeCartesianCategory| [ c , c' ]) →
+          Cᴰ [ f ][ elim-F-ob c , elim-F-ob c' ]
+        elim-F-hom (↑ₑ t) = ı-hom t
+        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 g h i) =
+          Cᴰ.⋆Assocᴰ (elim-F-hom f) (elim-F-hom g) (elim-F-hom h) i
+        elim-F-hom (isSetExp f g p q i j) =
+          isOfHLevel→isOfHLevelDep 2 (λ _ → 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-F-hom !ₑ = !tᴰ _
+        -- TODO: Why does this need rectify?
+        elim-F-hom (⊤η f i) =
+          R.≡[]-rectify {p' = ⊤η f} (𝟙ηᴰ (elim-F-hom f)) i
+        elim-F-hom π₁ = π₁ᴰ
+        elim-F-hom π₂ = π₂ᴰ
+        elim-F-hom ⟨ f₁ , f₂ ⟩ = elim-F-hom f₁ ,pᴰ elim-F-hom f₂
+        elim-F-hom (×β₁ {t = f₁}{t' = f₂} i) =
+          ×β₁ᴰ {f₁ᴰ = elim-F-hom f₁} {f₂ᴰ = elim-F-hom f₂} i
+        elim-F-hom (×β₂ {t = f₁}{t' = f₂} i) =
+          ×β₂ᴰ {f₁ᴰ = elim-F-hom f₁} {f₂ᴰ = elim-F-hom f₂} i
+        -- TODO: Why do we need this rectify too?
+        elim-F-hom (×η {t = f} i) =
+          R.≡[]-rectify {p' = ×η {t = f}} (×ηᴰ {fᴰ = elim-F-hom f}) i
 
         elim : GlobalSection Cᴰ
         elim .F-obᴰ = elim-F-ob
         elim .F-homᴰ = elim-F-hom
         elim .F-idᴰ = refl
         elim .F-seqᴰ _ _ = refl
+
+  module _
+    {D : Category ℓD ℓD'}
+    {F : Functor |FreeCartesianCategory| D}
+    {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+    where
+    module _
+      (lt : LiftedTerminal (reindex Dᴰ F)
+        (terminalToUniversalElement (FreeCartesianCategory .snd .fst)))
+      (lbp : LiftedBinProducts (reindex Dᴰ F)
+        (BinProductsToBinProducts' _ (FreeCartesianCategory .snd .snd)))
+      where
+      private
+        module Dᴰ = Categoryᴰ Dᴰ
+        CCᴰ : CartesianCategoryᴰ _ ℓDᴰ ℓDᴰ'
+        CCᴰ = reindex Dᴰ F , (lt , lbp)
+      module _
+        (ϕ : (o : Q .fst) → Dᴰ.ob[ F ⟅ ↑ o ⟆ ])
+        (ψ : (e : Q .snd .mor) →
+               Dᴰ.Hom[ F ⟪ ↑ₑ e ⟫ ][
+               elim-F-ob CCᴰ ϕ (Q.Dom e) ,
+               elim-F-ob CCᴰ ϕ (Q.Cod e)
+               ])
+        where
+        elimLocal' : Section F Dᴰ
+        elimLocal' = GlobalSectionReindex→Section Dᴰ F (elim CCᴰ ϕ ψ)
+
+    module _
+      (vt : VerticalTerminalAt Dᴰ (F ⟅ ⊤ ⟆))
+      (lift-π₁₂ : {c c' : Q.Ob}
+        (Fcᴰ : Categoryᴰ.ob[ Dᴰ ] (F ⟅ c ⟆))
+        (Fc'ᴰ : Categoryᴰ.ob[ Dᴰ ] (F ⟅ c' ⟆)) →
+        (CartesianOver Dᴰ Fcᴰ (F ⟪ π₁ ⟫) Σ.×
+        CartesianOver Dᴰ Fc'ᴰ (F ⟪ π₂ ⟫)))
+      (∧ : {c c' : Q.Ob}
+        (Fcᴰ : Categoryᴰ.ob[ Dᴰ ] (F ⟅ c ⟆))
+        (Fc'ᴰ : Categoryᴰ.ob[ Dᴰ ] (F ⟅ c' ⟆)) →
+        VerticalBinProductsAt Dᴰ
+          (lift-π₁₂ Fcᴰ Fc'ᴰ .fst .CartesianOver.f*cᴰ' ,
+          lift-π₁₂ Fcᴰ Fc'ᴰ .snd .CartesianOver.f*cᴰ'))
+      where
+      private
+        module Dᴰ = Categoryᴰ Dᴰ
+        lt : LiftedTerminal (reindex Dᴰ F)
+            (terminalToUniversalElement (FreeCartesianCategory .snd .fst))
+        lt = LiftedTerminalReindex vt
+        lbp : LiftedBinProducts (reindex Dᴰ F)
+            (BinProductsToBinProducts' _ (FreeCartesianCategory .snd .snd))
+        lbp = LiftedBinProdsReindex
+          (BinProductsToBinProducts' _ (FreeCartesianCategory .snd .snd))
+          lift-π₁₂ ∧
+        CCᴰ : CartesianCategoryᴰ _ ℓDᴰ ℓDᴰ'
+        CCᴰ = reindex Dᴰ F , (lt , lbp)
+      module _
+        (ϕ : (o : Q .fst) → Dᴰ.ob[ F ⟅ ↑ o ⟆ ])
+        (ψ : (e : Q .snd .mor) →
+          Dᴰ.Hom[ F ⟪ ↑ₑ e ⟫ ][
+            elim-F-ob CCᴰ ϕ (Q.Dom e) ,
+            elim-F-ob CCᴰ ϕ (Q.Cod e)
+          ]) where
+        elimLocal : Section F Dᴰ
+        elimLocal = elimLocal' lt lbp ϕ ψ
+
+  module _ (CC : CartesianCategory ℓC ℓC')
+    (ϕ : (o : Q .fst) → CC .fst .ob)
+    where
+    ϕ* : Q.Ob → CC .fst .ob
+    ϕ* = elim-F-ob
+      (weaken |FreeCartesianCategory| (CC .fst) ,
+      termWeaken (terminalToUniversalElement (FreeCartesianCategory .snd .fst))
+        (terminalToUniversalElement (CC .snd .fst)) ,
+      binprodWeaken
+        (BinProductsToBinProducts' _ (FreeCartesianCategory .snd .snd))
+        (BinProductsToBinProducts' _ (CC .snd .snd)))
+      ϕ
+    module _ (ψ : (e : Q .snd .mor) →
+      CC .fst [
+        ϕ* (Q.Dom e) ,
+        ϕ* (Q.Cod e)
+      ])
+      where
+      rec : Functor |FreeCartesianCategory| (CC .fst)
+      rec = introS⁻ (elim
+        ((weaken |FreeCartesianCategory| (CC .fst)) ,
+          termWeaken _ (terminalToUniversalElement (CC .snd .fst)) ,
+          binprodWeaken
+            (BinProductsToBinProducts' _ (FreeCartesianCategory .snd .snd))
+            (BinProductsToBinProducts' _ (CC .snd .snd)))
+        ϕ ψ)
diff --git a/Cubical/Categories/Constructions/Free/Category/Quiver.agda b/Cubical/Categories/Constructions/Free/Category/Quiver.agda
@@ -17,7 +17,7 @@ open import Cubical.Data.Graph.Displayed as Graph hiding (Section)
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Constructions.BinProduct as BP
 open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
 open import Cubical.Categories.Displayed.Instances.Path
 open import Cubical.Categories.Displayed.Properties as Reindex
 open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex

diff --git a/Cubical/Categories/Constructions/Presented.agda b/Cubical/Categories/Constructions/Presented.agda
@@ -16,13 +16,13 @@ open import Cubical.HITs.SetQuotients as SetQuotient
   renaming ([_] to [_]q) hiding (rec; elim)
 
 open import Cubical.Categories.Constructions.Quotient as CatQuotient
-open import Cubical.Categories.Displayed.Constructions.Weaken as Weaken
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Weaken
 open import Cubical.Categories.Constructions.Free.Category.Quiver as Free
   hiding (rec; elim)
 open import Cubical.Categories.Constructions.Quotient.More as CatQuotient
   hiding (elim)
 open import Cubical.Categories.Displayed.Base
-open import Cubical.Categories.Displayed.Constructions.Weaken
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base
 open import Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 open import Cubical.Categories.Displayed.Section.Base
 

diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Properties.agda
@@ -220,13 +220,33 @@ module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}
         VerticalBinProductsAt Dᴰ (lift-π₁ .f*cᴰ' , lift-π₂ .f*cᴰ')
       VerticalBinProds→ϕ[π₁x]∧ψ[π₂x] = vbps _
 
+  module _
+    (prods : BinProducts' C) where
+    private module B = BinProducts'Notation _ prods
+    module _
+      (lift-π₁₂ : {c c' : C .ob}
+        (Fcᴰ : Dᴰ.ob[ F ⟅ c ⟆ ])(Fc'ᴰ : Dᴰ.ob[ F ⟅ c' ⟆ ]) →
+        CartesianOver Dᴰ Fcᴰ (F ⟪ B.π₁ {a = c} {b = c'} ⟫) ×
+        CartesianOver Dᴰ Fc'ᴰ (F ⟪ B.π₂ {a = c} {b = c'} ⟫))
+      (vbp : {c c' : C .ob} (Fcᴰ : Dᴰ.ob[ F ⟅ c ⟆ ])(Fc'ᴰ : Dᴰ.ob[ F ⟅ c' ⟆ ]) →
+        VerticalBinProductsAt Dᴰ (lift-π₁₂ Fcᴰ Fc'ᴰ .fst .f*cᴰ' ,
+          lift-π₁₂ Fcᴰ Fc'ᴰ .snd .f*cᴰ'))
+      where
+      LiftedBinProdsReindex : LiftedBinProducts (reindex Dᴰ F) prods
+      LiftedBinProdsReindex (Fcᴰ , Fc'ᴰ) = LiftedBinProdReindex (prods _)
+        (lift-π₁₂ Fcᴰ Fc'ᴰ .fst)
+        (lift-π₁₂ Fcᴰ Fc'ᴰ .snd)
+        (vbp Fcᴰ Fc'ᴰ)
+
   module _ (prods : BinProducts' C)
-    (fib : isFibration Dᴰ)(vbps : VerticalBinProducts Dᴰ) where
-    LiftedBinProdsReindex : LiftedBinProducts (reindex Dᴰ F) prods
-    LiftedBinProdsReindex (Fcᴰ , Fc'ᴰ) = LiftedBinProdReindex (prods _)
-      (isFib→F⟪π₁⟫* (prods _) Fcᴰ fib)
-      (isFib→F⟪π₂⟫* (prods _) Fc'ᴰ fib)
-      (VerticalBinProds→ϕ[π₁x]∧ψ[π₂x] (prods _)
+    (fib : isFibration Dᴰ)
+    (vbps : VerticalBinProducts Dᴰ) where
+    LiftedBinProdsReindex' : LiftedBinProducts (reindex Dᴰ F) prods
+    LiftedBinProdsReindex' = LiftedBinProdsReindex prods
+      (λ Fcᴰ Fc'ᴰ →
+        isFib→F⟪π₁⟫* (prods _) Fcᴰ fib , isFib→F⟪π₂⟫* (prods _) Fc'ᴰ fib)
+      (λ Fcᴰ Fc'ᴰ → VerticalBinProds→ϕ[π₁x]∧ψ[π₂x]
+        (prods _)
         (isFib→F⟪π₁⟫* (prods _) Fcᴰ fib)
         (isFib→F⟪π₂⟫* (prods _) Fc'ᴰ fib)
         vbps)
diff --git a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryL.agda
@@ -18,7 +18,7 @@ open import Cubical.Categories.Displayed.Reasoning
 open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex
   hiding (introS)
 open import Cubical.Categories.Displayed.Constructions.Reindex.Eq as ReindexEq
-open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
   hiding (introS; introF)
 open import Cubical.Categories.Displayed.Properties
 open import Cubical.Categories.Displayed.Functor

diff --git a/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda b/Cubical/Categories/Displayed/Constructions/SimpleTotalCategoryR.agda
@@ -29,7 +29,7 @@ open import Cubical.Categories.Displayed.Section.Base
 open import Cubical.Categories.Displayed.Reasoning
 open import Cubical.Categories.Displayed.Constructions.Reindex as Reindex
   hiding (introS; introF)
-open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
   hiding (introS; introF)
 open import Cubical.Categories.Displayed.Properties
 open import Cubical.Categories.Displayed.Functor

diff --git a/Cubical/Categories/Displayed/Constructions/Slice.agda b/Cubical/Categories/Displayed/Constructions/Slice.agda
@@ -26,7 +26,7 @@ open import Cubical.Categories.Constructions.BinProduct as BP
 open import Cubical.Categories.Constructions.BinProduct.More as BP
 open import Cubical.Categories.Functor.Base
 open import Cubical.Categories.Displayed.Base as Disp
-open import Cubical.Categories.Displayed.Constructions.Weaken as Wk
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base as Wk
 open import Cubical.Categories.Displayed.Constructions.Reindex.Eq as Reindex
 open import Cubical.Categories.Displayed.BinProduct
 open import Cubical.Categories.Displayed.Constructions.BinProduct.More as BPᴰ

diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda
@@ -4,17 +4,20 @@ module Cubical.Categories.Displayed.Constructions.Weaken.Properties where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
+open import Cubical.Foundations.Equiv
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor
 open import Cubical.Categories.Limits.Terminal.More
+open import Cubical.Categories.Limits.BinProduct.More
 open import Cubical.Categories.Presheaf
 
 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.Displayed.Limits.Terminal
+open import Cubical.Categories.Displayed.Limits.BinProduct
 open import Cubical.Categories.Constructions.TotalCategory as TC
   hiding (intro)
 open import Cubical.Categories.Constructions.TotalCategory.More as TC
@@ -28,10 +31,15 @@ private
 open Categoryᴰ
 open UniversalElementᴰ
 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 .vertexᴰ = termD .vertex
-  termWeaken .elementᴰ = termD .element
-  termWeaken .universalᴰ = termD .universal _
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where
+  module _ (termC : Terminal' C) (termD : Terminal' D) where
+    termWeaken : LiftedTerminal (weaken C D) termC
+    termWeaken .vertexᴰ = termD .vertex
+    termWeaken .elementᴰ = termD .element
+    termWeaken .universalᴰ = termD .universal _
+  module _ (prodC : BinProducts' C)(prodD : BinProducts' D) where
+    private module B = BinProducts'Notation _ prodD
+    binprodWeaken : LiftedBinProducts (weaken C D) prodC
+    binprodWeaken _ .vertexᴰ = prodD _ .vertex
+    binprodWeaken _ .elementᴰ = prodD _ .element
+    binprodWeaken _ .universalᴰ = prodD _ .universal _
diff --git a/Cubical/Categories/Displayed/Functor/More.agda b/Cubical/Categories/Displayed/Functor/More.agda
@@ -12,7 +12,7 @@ import      Cubical.Data.Equality.More as Eq
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Properties
 open import Cubical.Categories.Displayed.Functor
-open import Cubical.Categories.Displayed.Constructions.Weaken
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base
 import      Cubical.Categories.Displayed.Reasoning as HomᴰReasoning
 
 private

diff --git a/Cubical/Categories/Displayed/Limits/BinProduct.agda b/Cubical/Categories/Displayed/Limits/BinProduct.agda
@@ -96,7 +96,8 @@ module LiftedBinProductsNotation
            where
     private
       ,pᴰ-contr = bpᴰ (d₁ , d₂) .universalᴰ .equiv-proof
-        (R.reind (sym ×β₁) (fᴰ Cᴰ.⋆ᴰ π₁ᴰ) , R.reind (sym ×β₂) (fᴰ Cᴰ.⋆ᴰ π₂ᴰ)) .snd
+        (R.reind (sym ×β₁) (fᴰ Cᴰ.⋆ᴰ π₁ᴰ) ,
+          R.reind (sym ×β₂) (fᴰ Cᴰ.⋆ᴰ π₂ᴰ)) .snd
         ((R.reind (×η {f = f}) fᴰ) , ΣPathP
         ( R.≡[]-rectify (R.≡[]∙ _ _
           (R.≡[]⋆ _ _ (R.reind-filler-sym (sym ×η) fᴰ) (refl {x = π₁ᴰ}))

diff --git a/Cubical/Categories/Profunctor/FunctorComprehension.agda b/Cubical/Categories/Profunctor/FunctorComprehension.agda
@@ -54,7 +54,7 @@ open import Cubical.Categories.Instances.Functors.More
 open import Cubical.Categories.Displayed.Functor
 open import Cubical.Categories.Displayed.Constructions.Comma
 open import Cubical.Categories.Displayed.Constructions.Graph
-open import Cubical.Categories.Displayed.Constructions.Weaken
+open import Cubical.Categories.Displayed.Constructions.Weaken.Base
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.HLevels
 open import Cubical.Categories.Displayed.HLevels.More