From 2e6ba2bda80155c014d997e821f2961487f0a939 Mon Sep 17 00:00:00 2001
From: Josselin Poiret <dev@jpoiret.xyz>
Date: Fri, 6 Sep 2024 17:11:30 +0200
Subject: [PATCH 1/2] Rework displayed category reasoning.

This new technique is both more performant, more readable and reduces
boilerplate.
---
 Cubical/Categories/Category/Base.agda       |   4 +
 Cubical/Categories/Displayed/Reasoning.agda | 126 ++++++++------------
 2 files changed, 54 insertions(+), 76 deletions(-)

diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda
index 427b17b94f..280bea3b62 100644
--- a/Cubical/Categories/Category/Base.agda
+++ b/Cubical/Categories/Category/Base.agda
@@ -29,6 +29,10 @@ record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   _∘_ : ∀ {x y z} (g : Hom[ y , z ]) (f : Hom[ x , y ]) → Hom[ x , z ]
   g ∘ f = f ⋆ g
 
+  ⟨_⟩⋆⟨_⟩ : {x y z : ob} {f f' : Hom[ x , y ]} {g g' : Hom[ y , z ]}
+          → f ≡ f' → g ≡ g' → f ⋆ g ≡ f' ⋆ g'
+  ⟨ ≡f ⟩⋆⟨ ≡g ⟩ = cong₂ _⋆_ ≡f ≡g
+
   infixr 9 _⋆_
   infixr 9 _∘_
 
diff --git a/Cubical/Categories/Displayed/Reasoning.agda b/Cubical/Categories/Displayed/Reasoning.agda
index ee964baa8b..223d4ef8c1 100644
--- a/Cubical/Categories/Displayed/Reasoning.agda
+++ b/Cubical/Categories/Displayed/Reasoning.agda
@@ -1,3 +1,19 @@
+{-
+Helping equational reasoning in displayed categories.
+
+The main proof engineering insight here is that we don't want to let Agda infer
+metavariables all the time for the base paths.
+The naive approach would be to work with the indexed (f ≡[ p ] g), where the p
+ends up being inferred for every operation (we don't want to supply the
+equations over which the displayed ones live). However, the performance hit is
+enormous, making it completely unusable for longer chains of equalities!
+
+Instead, we just work in the total category (∫C Cᴰ), giving access to the
+usual categorical reasoning tools, and project out at the end. This way, we
+carry around the base morphisms and paths as *data* rather than just re-inferring
+them all the time. This has very good performance while letting us freely use
+implicit arguments for e.g. ⋆Assoc.
+-}
 {-# OPTIONS --safe #-}
 
 open import Cubical.Foundations.Prelude
@@ -5,7 +21,10 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Transport
 
+open import Cubical.Data.Sigma
+
 open import Cubical.Categories.Category.Base
+open import Cubical.Categories.Constructions.TotalCategory.Base
 open import Cubical.Categories.Displayed.Base
 
 module Cubical.Categories.Displayed.Reasoning
@@ -18,91 +37,46 @@ module Cubical.Categories.Displayed.Reasoning
   private module C = Category C
   open Category hiding (_∘_)
 
+  -- We give access to usual categorical operations of the total category
+  -- directly through this module.
+  open Category (∫C Cᴰ) public
+
+  -- Shorthand to introduce a displayed equality into the reasoning machine
+  ≡in : {a b : C.ob} {f g : C [ a , b ]}
+        {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
+        {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
+        {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
+        {p : f ≡ g}
+      → (fᴰ ≡[ p ] gᴰ)
+      → (f , fᴰ) ≡ (g , gᴰ)
+  ≡in e = ΣPathP (_ , e)
+
+  -- Shorthand to produce a displayed equality out of the reasoning machine
+  ≡out : {a b : C.ob} {f g : C [ a , b ]}
+         {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
+         {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
+         {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
+       → (e : (f , fᴰ) ≡ (g , gᴰ))
+       → (fᴰ ≡[ fst (PathPΣ e) ] gᴰ)
+  ≡out e = snd (PathPΣ e)
+
+  -- Reindexing displayed morphisms along an equality in the base
   reind : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
       {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
     → Hom[ f ][ aᴰ , bᴰ ] → Hom[ g ][ aᴰ , bᴰ ]
   reind p = subst Hom[_][ _ , _ ] p
 
+  -- Filler for the above, directly in the reasoning machine
   reind-filler : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
       {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      (f : Hom[ f ][ aᴰ , bᴰ ])
-    → f ≡[ p ] reind p f
-  reind-filler p = subst-filler Hom[_][ _ , _ ] p
-
-  reind-filler-sym : {a b : C.ob} {f g : C [ a , b ]} (p : f ≡ g)
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      (f : Hom[ g ][ aᴰ , bᴰ ])
-    → reind (sym p) f ≡[ p ] f
-  reind-filler-sym p = symP ∘ reind-filler (sym p)
+      (fᴰ : Hom[ f ][ aᴰ , bᴰ ])
+    → (f , fᴰ) ≡ (g , reind p fᴰ)
+  reind-filler p fᴰ = ΣPathP (p , subst-filler Hom[_][ _ , _ ] p fᴰ)
 
-  ≡[]-rectify : {a b : C.ob} {f g : C [ a , b ]} {p p' : f ≡ g}
+  -- Rectify the base equality of dependent equalities to whatever we want
+  rectify : {a b : C.ob} {f g : C [ a , b ]} {p p' : f ≡ g}
       {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
       {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
       {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
     → fᴰ ≡[ p ] gᴰ → fᴰ ≡[ p' ] gᴰ
-  ≡[]-rectify {fᴰ = fᴰ} {gᴰ = gᴰ} = subst (fᴰ ≡[_] gᴰ) (C.isSetHom _ _ _ _)
-
-  ≡[]∙ : {a b : C.ob} {f g h : C [ a , b ]}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
-      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
-      {hᴰ : Hom[ h ][ aᴰ , bᴰ ]}
-      (p : f ≡ g) (q : g ≡ h)
-    → fᴰ ≡[ p ] gᴰ
-    → gᴰ ≡[ q ] hᴰ → fᴰ ≡[ p ∙ q ] hᴰ
-  ≡[]∙ {fᴰ = fᴰ} {hᴰ = hᴰ} p q eq1 eq2 =
-    subst
-      (λ p → PathP (λ i → p i) fᴰ hᴰ)
-      (sym $ congFunct Hom[_][ _ , _ ] p q)
-      (compPathP eq1 eq2)
-
-  infixr 30 ≡[]∙
-  syntax ≡[]∙ p q eq1 eq2 = eq1 [ p ]∙[ q ] eq2
-
-  ≡[]⋆ : {a b c : C.ob} {f g : C [ a , b ]} {h i : C [ b , c ]}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
-      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
-      {hᴰ : Hom[ h ][ bᴰ , cᴰ ]}
-      {iᴰ : Hom[ i ][ bᴰ , cᴰ ]}
-      (p : f ≡ g) (q : h ≡ i)
-    → fᴰ ≡[ p ] gᴰ → hᴰ ≡[ q ] iᴰ → fᴰ ⋆ᴰ hᴰ ≡[ cong₂ C._⋆_ p q ] gᴰ ⋆ᴰ iᴰ
-  ≡[]⋆ _ _ = congP₂ (λ _ → _⋆ᴰ_)
-
-  infixr 30 ≡[]⋆
-  syntax ≡[]⋆ p q eq1 eq2 = eq1 [ p ]⋆[ q ] eq2
-
-  reind-rectify : {a b : C.ob} {f g : C [ a , b ]} {p p' : f ≡ g}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
-    → reind p fᴰ ≡ reind p' fᴰ
-  reind-rectify {fᴰ = fᴰ} = cong (λ p → reind p fᴰ) (C.isSetHom _ _ _ _)
-
-  reind-contractʳ : {a b c : C.ob} {f g : C [ a , b ]} {h : C [ b , c ]}
-      {p : f ≡ g}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]} {hᴰ : Hom[ h ][ bᴰ , cᴰ ]}
-    → reind (cong (C._⋆ h) p) (fᴰ ⋆ᴰ hᴰ) ≡ reind p fᴰ ⋆ᴰ hᴰ
-  reind-contractʳ {hᴰ = hᴰ} = fromPathP $
-    congP (λ _ → _⋆ᴰ hᴰ) (transport-filler _ _)
-
-  reind-comp : {a b : C.ob} {f g h : C [ a , b ]} {p : f ≡ g} {q : g ≡ h}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
-    → reind (p ∙ q) fᴰ ≡ reind q (reind p fᴰ)
-  reind-comp = substComposite Hom[_][ _ , _ ] _ _ _
-
-  reind-contractˡ : {a b c : C.ob} {f : C [ a , b ]} {g h : C [ b , c ]}
-      {p : g ≡ h}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {cᴰ : ob[ c ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]} {gᴰ : Hom[ g ][ bᴰ , cᴰ ]}
-    → reind (cong (f C.⋆_) p) (fᴰ ⋆ᴰ gᴰ) ≡ fᴰ ⋆ᴰ reind p gᴰ
-  reind-contractˡ {fᴰ = fᴰ} = fromPathP $
-    congP (λ _ → fᴰ ⋆ᴰ_) (transport-filler _ _)
-
-  ≡→≡[] : {a b : C.ob} {f g : C [ a , b ]} {p : f ≡ g}
-      {aᴰ : ob[ a ]} {bᴰ : ob[ b ]}
-      {fᴰ : Hom[ f ][ aᴰ , bᴰ ]}
-      {gᴰ : Hom[ g ][ aᴰ , bᴰ ]}
-    → reind p fᴰ ≡ gᴰ → fᴰ ≡[ p ] gᴰ
-  ≡→≡[] = toPathP
+  rectify {fᴰ = fᴰ} {gᴰ = gᴰ} = subst (fᴰ ≡[_] gᴰ) (C.isSetHom _ _ _ _)

From a845cdb8c92f0e9a552ac7df21f40d7cc4fe22c0 Mon Sep 17 00:00:00 2001
From: Josselin Poiret <dev@jpoiret.xyz>
Date: Fri, 6 Sep 2024 18:02:34 +0200
Subject: [PATCH 2/2] Adapt proofs to new displayed category reasoning.

---
 .../TotalCategory/Properties.agda             |   4 +-
 Cubical/Categories/Displayed/Cartesian.agda   | 121 +++++++-----------
 .../Displayed/Constructions/Reindex/Base.agda |  44 +++----
 .../Categories/Displayed/Section/Base.agda    |  29 +++--
 4 files changed, 80 insertions(+), 118 deletions(-)

diff --git a/Cubical/Categories/Constructions/TotalCategory/Properties.agda b/Cubical/Categories/Constructions/TotalCategory/Properties.agda
index 2c19d316b1..c00d1550e6 100644
--- a/Cubical/Categories/Constructions/TotalCategory/Properties.agda
+++ b/Cubical/Categories/Constructions/TotalCategory/Properties.agda
@@ -115,7 +115,7 @@ module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
     recᴰ : Functorᴰ F Cᴰ Dᴰ
     recᴰ .F-obᴰ {x} xᴰ = Fᴰ .F-obᴰ (x , xᴰ)
     recᴰ .F-homᴰ {f = f} fᴰ = Fᴰ .F-homᴰ (f , fᴰ)
-    recᴰ .F-idᴰ = R.≡[]-rectify (Fᴰ .F-idᴰ)
+    recᴰ .F-idᴰ = R.rectify (Fᴰ .F-idᴰ)
     recᴰ .F-seqᴰ {x} {y} {z} {f} {g} {xᴰ} {yᴰ} {zᴰ} fᴰ gᴰ =
-      R.≡[]-rectify (Fᴰ .F-seqᴰ (f , fᴰ) (g , gᴰ))
+      R.rectify (Fᴰ .F-seqᴰ (f , fᴰ) (g , gᴰ))
 
diff --git a/Cubical/Categories/Displayed/Cartesian.agda b/Cubical/Categories/Displayed/Cartesian.agda
index af997c155a..6dedcb8f00 100644
--- a/Cubical/Categories/Displayed/Cartesian.agda
+++ b/Cubical/Categories/Displayed/Cartesian.agda
@@ -149,39 +149,27 @@ module Covariant
     module _ (fᴰ-isIsoᴰ : isIsoᴰ Cᴰ f-isIso fᴰ) where
       open isIsoᴰ fᴰ-isIsoᴰ
 
-      private basepath : {c : B.ob} (g : B [ b , c ]) → inv B.⋆ f B.⋆ g ≡ g
-      basepath g =
-          sym (B.⋆Assoc _ _ _)
-        ∙ cong (B._⋆ g) sec
-        ∙ B.⋆IdL _
-      {-# INLINE basepath #-}
-
       isIsoᴰ→isOpcartesian : isOpcartesian fᴰ
       isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .fst .fst =
         R.reind
-          (basepath g)
+          ( sym (B.⋆Assoc _ _ _)
+          ∙ B.⟨ sec ⟩⋆⟨ refl ⟩
+          ∙ B.⋆IdL _)
           (invᴰ ⋆ᴰ fgᴰ)
       isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .fst .snd =
-        R.≡[]-rectify $
-          (refl R.[ refl ]⋆[ sym (basepath g) ] symP (R.reind-filler (basepath g) _))
-            R.[ _ ]∙[ _ ]
-          symP (Cᴰ.⋆Assocᴰ fᴰ invᴰ fgᴰ)
-            R.[ sym $ B.⋆Assoc f inv (f B.⋆ g) ]∙[ _ ]
-          (retᴰ R.[ ret ]⋆[ refl ] refl)
-            R.[ _ ]∙[ _ ]
-          Cᴰ.⋆IdLᴰ fgᴰ
+        R.rectify $ R.≡out $
+            R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
+          ∙ sym (R.⋆Assoc _ _ _)
+          ∙ R.⟨ R.≡in retᴰ ⟩⋆⟨ refl ⟩
+          ∙ R.⋆IdL _
       isIsoᴰ→isOpcartesian g .equiv-proof fgᴰ .snd (gᴰ , gᴰ-infib) =
         Σ≡Prop (λ _ → isOfHLevelPathP' 1 Cᴰ.isSetHomᴰ _ _) $
-          R.≡[]-rectify $
-            symP (R.reind-filler (basepath g) _)
-              R.[ sym (basepath g) ]∙[ _ ]
-            (refl R.[ refl ]⋆[ refl ] symP gᴰ-infib)
-              R.[ _ ]∙[ _ ]
-            symP (Cᴰ.⋆Assocᴰ invᴰ fᴰ gᴰ)
-              R.[ sym (B.⋆Assoc inv f g) ]∙[ _ ]
-            (secᴰ R.[ sec ]⋆[ refl ] refl)
-              R.[ _ ]∙[ _ ]
-            Cᴰ.⋆IdLᴰ gᴰ
+          R.rectify $ R.≡out $
+              sym (R.reind-filler _ _)
+            ∙ R.⟨ refl ⟩⋆⟨ sym $ R.≡in gᴰ-infib ⟩
+            ∙ sym (R.⋆Assoc _ _ _)
+            ∙ R.⟨ R.≡in secᴰ ⟩⋆⟨ refl ⟩
+            ∙ R.⋆IdL _
 
     module _ (opcart : isOpcartesian fᴰ) where
       open isIsoᴰ
@@ -189,33 +177,26 @@ module Covariant
       isOpcartesian→isIsoᴰ : isIsoᴰ Cᴰ f-isIso fᴰ
       isOpcartesian→isIsoᴰ .invᴰ =
         opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .fst
-      isOpcartesian→isIsoᴰ .retᴰ = R.≡[]-rectify $
-        opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .snd
-          R.[ _ ]∙[ ret ]
-        R.reind-filler-sym ret idᴰ
+      isOpcartesian→isIsoᴰ .retᴰ = R.rectify $ R.≡out $
+          R.≡in (opcart inv .equiv-proof (R.reind (sym ret) idᴰ) .fst .snd)
+        ∙ sym (R.reind-filler _ _)
       isOpcartesian→isIsoᴰ .secᴰ =
         let
           ≡-any-two-in-fib = isContr→isProp $
             opcart (inv B.⋆ f) .equiv-proof
               (fᴰ ⋆ᴰ (isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ)
           -- Reindexed idᴰ is a valid lift for the composition.
-          idᴰ-in-fib = R.≡[]-rectify $
-            (refl {x = fᴰ} R.[ refl ]⋆[ _ ] R.reind-filler-sym sec idᴰ)
-              R.[ _ ]∙[ _ ]
-            ⋆IdRᴰ fᴰ
-              R.[ B.⋆IdR f ]∙[ _ ]
-            symP (⋆IdLᴰ fᴰ)
-              R.[ sym (B.⋆IdL f) ]∙[ _ ]
-            (symP (isOpcartesian→isIsoᴰ .retᴰ) R.[ sym ret ]⋆[ refl ] refl {x = fᴰ})
-              R.[ _ ]∙[ _ ]
-            ⋆Assocᴰ fᴰ (isOpcartesian→isIsoᴰ .invᴰ) fᴰ
-        in R.≡[]-rectify $
-        (cong fst $ ≡-any-two-in-fib
-          ((isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ , refl)
-          (R.reind (sym sec) idᴰ , idᴰ-in-fib))
-
-          R.[ _ ]∙[ _ ]
-        R.reind-filler-sym sec idᴰ
+          idᴰ-in-fib = R.rectify $ R.≡out $
+              R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
+            ∙ R.⋆IdR _
+            ∙ sym (R.⋆IdL _)
+            ∙ R.⟨ sym $ R.≡in $ isOpcartesian→isIsoᴰ .retᴰ ⟩⋆⟨ refl ⟩
+            ∙ R.⋆Assoc _ _ _
+        in R.rectify $ R.≡out $
+            R.≡in (cong fst $ ≡-any-two-in-fib
+              ((isOpcartesian→isIsoᴰ .invᴰ) ⋆ᴰ fᴰ , refl)
+              (R.reind (sym sec) idᴰ , idᴰ-in-fib))
+          ∙ sym (R.reind-filler _ _)
 
   -- Construction of the substitution functor for a general opfibration.
   module _
@@ -236,17 +217,16 @@ module Covariant
            f ⋆ᴰ cleavage σ y .snd .fst)
     substituteArrow f =
         map-snd
-          (λ p → R.≡[]-rectify $
-            p
-              R.[ _ ]∙[ sym (B.⋆IdL _ ∙ sym (B.⋆IdR _)) ]
-            symP (R.reind-filler _ _))
+          (λ p → R.rectify $ R.≡out $
+              R.≡in p
+            ∙ sym (R.reind-filler _ _))
           (cart .fst)
       , λ g' →
           Σ≡Prop
             (λ _ → isOfHLevelPathP' 1 isSetHomᴰ _ _)
             (cong fst $ cart .snd $
               map-snd
-                (λ p → R.≡[]-rectify $ p R.[ _ ]∙[ _ ] R.reind-filler _ _)
+                (λ p → R.rectify $ R.≡out $ R.≡in p ∙ R.reind-filler _ _)
                 g')
       where
         cart : isContr (Σ _ _)
@@ -260,33 +240,22 @@ module Covariant
     substitutionFunctor .F-id {x} = cong fst $
       substituteArrow (VerticalCategory Cᴰ a .Category.id) .snd $
         VerticalCategory Cᴰ b .Category.id
-      , R.≡[]-rectify
-          ((refl R.[ refl ]⋆[ refl ] symP (R.reind-filler refl idᴰ))
-             R.[ cong₂ B._⋆_ refl refl ]∙[ _ ]
-           ⋆IdRᴰ (cleavage σ x .snd .fst)
-             R.[ B.⋆IdR σ ]∙[ _ ]
-           symP (⋆IdLᴰ (cleavage σ x .snd .fst))
-             R.[ sym (B.⋆IdL σ) ]∙[ _ ]
-           (R.reind-filler refl idᴰ R.[ refl ]⋆[ refl ] refl))
+      , (R.rectify $ R.≡out $
+            R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
+          ∙ R.⋆IdR _
+          ∙ sym (R.⋆IdL _)
+          ∙ R.⟨ R.reind-filler _ _ ⟩⋆⟨ refl ⟩)
     substitutionFunctor .F-seq {x} {y} {z} f g = cong fst $
       substituteArrow (VerticalCategory Cᴰ a .Category._⋆_ f g) .snd $
         VerticalCategory Cᴰ b .Category._⋆_ (stepf .fst) (stepg .fst)
-      , R.≡[]-rectify
-          ((refl
-              R.[ refl ]⋆[ sym (B.⋆IdL B.id) ]
-            R.reind-filler-sym (sym $ B.⋆IdL B.id) (stepf .fst ⋆ᴰ stepg .fst))
-             R.[ cong₂ B._⋆_ refl (sym $ B.⋆IdL B.id) ]∙[ _ ]
-           symP (⋆Assocᴰ (cleavage σ x .snd .fst) (stepf .fst) (stepg .fst))
-             R.[ sym (B.⋆Assoc σ B.id B.id) ]∙[ _ ]
-           (stepf .snd R.[ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ]⋆[ refl ] refl)
-             R.[ cong₂ B._⋆_ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) refl ]∙[ _ ]
-           ⋆Assocᴰ f (cleavage σ y .snd .fst) (stepg .fst)
-             R.[ B.⋆Assoc B.id σ B.id ]∙[ _ ]
-           (refl R.[ refl ]⋆[ (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ] stepg .snd)
-             R.[ cong₂ B._⋆_ refl (B.⋆IdR σ ∙ sym (B.⋆IdL σ)) ]∙[ _ ]
-           symP (⋆Assocᴰ f g (cleavage σ z .snd .fst))
-             R.[ sym (B.⋆Assoc B.id B.id σ) ]∙[ cong₂ B._⋆_ (B.⋆IdL B.id) refl ]
-           (R.reind-filler (B.⋆IdL B.id) (f ⋆ᴰ g) R.[ B.⋆IdL B.id ]⋆[ refl ] refl))
+      , (R.rectify $ R.≡out $
+            R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ _ ⟩
+          ∙ sym (R.⋆Assoc _ _ _)
+          ∙ R.⟨ R.≡in $ stepf .snd ⟩⋆⟨ refl ⟩
+          ∙ R.⋆Assoc _ _ _
+          ∙ R.⟨ refl ⟩⋆⟨ R.≡in $ stepg .snd ⟩
+          ∙ sym (R.⋆Assoc _ _ _)
+          ∙ R.⟨ R.reind-filler _ _ ⟩⋆⟨ refl ⟩)
       where
         stepf = substituteArrow f .fst
         stepg = substituteArrow g .fst
diff --git a/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
index f1a292884d..466d7cc677 100644
--- a/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
+++ b/Cubical/Categories/Displayed/Constructions/Reindex/Base.agda
@@ -93,35 +93,27 @@ module _
   reindex .Categoryᴰ.Hom[_][_,_] f aᴰ bᴰ = Hom[ F-hom f ][ aᴰ , bᴰ ]
   reindex .Categoryᴰ.idᴰ = R.reind (sym F-id) idᴰ
   reindex .Categoryᴰ._⋆ᴰ_ fᴰ gᴰ = R.reind (sym $ F-seq _ _) (fᴰ ⋆ᴰ gᴰ)
-  reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (R.reind-filler-sym F-id idᴰ R.[ _ ]⋆[ refl ] refl)
-      R.[ _ ]∙[ _ ]
-    ⋆IdLᴰ fᴰ
-  reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (refl R.[ refl ]⋆[ _ ] R.reind-filler-sym F-id idᴰ)
-      R.[ _ ]∙[ _ ]
-    ⋆IdRᴰ fᴰ
-  reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.≡[]-rectify $
-    R.reind-filler-sym (F-seq _ _) _
-      R.[ _ ]∙[ _ ]
-    (R.reind-filler-sym (F-seq _ _) _ R.[ _ ]⋆[ refl ] refl)
-      R.[ _ ]∙[ _ ]
-    ⋆Assocᴰ fᴰ gᴰ hᴰ
-      R.[ _ ]∙[ _ ]
-    (refl R.[ refl ]⋆[ _ ] R.reind-filler (sym $ F-seq _ _) _)
-      R.[ _ ]∙[ _ ]
-    R.reind-filler (sym $ F-seq _ _) _
+  reindex .Categoryᴰ.⋆IdLᴰ fᴰ = R.rectify $ R.≡out $
+      sym (R.reind-filler _ _)
+    ∙ R.⟨ sym $ R.reind-filler _ idᴰ ⟩⋆⟨ refl ⟩
+    ∙ R.⋆IdL _
+  reindex .Categoryᴰ.⋆IdRᴰ fᴰ = R.rectify $ R.≡out $
+      sym (R.reind-filler _ _)
+    ∙ R.⟨ refl ⟩⋆⟨ sym $ R.reind-filler _ idᴰ ⟩
+    ∙ R.⋆IdR _
+  reindex .Categoryᴰ.⋆Assocᴰ fᴰ gᴰ hᴰ = R.rectify $ R.≡out $
+      sym (R.reind-filler _ _)
+    ∙ R.⟨ sym $ R.reind-filler _ _ ⟩⋆⟨ refl ⟩
+    ∙ R.⋆Assoc _ _ _
+    ∙ R.⟨ refl ⟩⋆⟨ R.reind-filler _ _ ⟩
+    ∙ R.reind-filler _ _
   reindex .Categoryᴰ.isSetHomᴰ = isSetHomᴰ
 
   π : Functorᴰ F reindex Dᴰ
   π .F-obᴰ = λ z → z
   π .F-homᴰ = λ z → z
-  π .F-idᴰ = symP (transport-filler _ _)
-  π .F-seqᴰ fᴰ gᴰ = symP (transport-filler _ _)
+  π .F-idᴰ = R.≡out $ sym (R.reind-filler _ _)
+  π .F-seqᴰ fᴰ gᴰ = R.≡out $ sym (R.reind-filler _ _)
 
   GlobalSectionReindex→Section : GlobalSection reindex → Section F Dᴰ
   GlobalSectionReindex→Section Fᴰ = compFunctorᴰGlobalSection π Fᴰ
@@ -142,9 +134,9 @@ module _
   introS : Section G (reindex Dᴰ F)
   introS .F-obᴰ = FGᴰ .F-obᴰ
   introS .F-homᴰ = FGᴰ .F-homᴰ
-  introS .F-idᴰ = R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-idᴰ) (R.reind-filler _ _))
+  introS .F-idᴰ = R.rectify $ R.≡out $ R.≡in (FGᴰ .F-idᴰ) ∙ (R.reind-filler _ _)
   introS .F-seqᴰ fᴰ gᴰ =
-    R.≡[]-rectify (R.≡[]∙ _ _ (FGᴰ .F-seqᴰ fᴰ gᴰ) (R.reind-filler _ _))
+    R.rectify $ R.≡out $ R.≡in (FGᴰ .F-seqᴰ fᴰ gᴰ) ∙ (R.reind-filler _ _)
 
 module _
   {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
diff --git a/Cubical/Categories/Displayed/Section/Base.agda b/Cubical/Categories/Displayed/Section/Base.agda
index 07cd1a7a82..5d6ea986db 100644
--- a/Cubical/Categories/Displayed/Section/Base.agda
+++ b/Cubical/Categories/Displayed/Section/Base.agda
@@ -73,6 +73,7 @@
 module Cubical.Categories.Displayed.Section.Base where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.HLevels
 
@@ -199,7 +200,7 @@ module _ {C : Category ℓC ℓC'}
       Gᴰ-idᴰ : (G : FunctorSingl F)
                (G-id : ∀ {x} → G .snd .fst (D .id {x}) ≡ C .id)
              →  ∀ {d} → Gᴰ-homᴰ G (D .id {d}) Cᴰ.≡[ G-id ] Cᴰ.idᴰ
-      Gᴰ-idᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-id = R.≡[]-rectify (Fᴰ .F-idᴰ)
+      Gᴰ-idᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-id = R.rectify (Fᴰ .F-idᴰ)
 
       Gᴰ-seqᴰ : (G : FunctorSingl F)
                 (G-seq : ∀ {d d' d''}(f : D [ d , d' ])(g : D [ d' , d'' ])
@@ -209,7 +210,7 @@ module _ {C : Category ℓC ℓC'}
               → Gᴰ-homᴰ G (f ⋆⟨ D ⟩ g)
                 Cᴰ.≡[ G-seq f g ] (Gᴰ-homᴰ G f Cᴰ.⋆ᴰ Gᴰ-homᴰ G g)
       Gᴰ-seqᴰ ((_ , Eq.refl), (_ , Eq.refl)) G-seq f g =
-        R.≡[]-rectify (Fᴰ .F-seqᴰ f g)
+        R.rectify (Fᴰ .F-seqᴰ f g)
 {-
 
    Composition of a Section and a Functor
@@ -238,12 +239,12 @@ module _ {B : Category ℓB ℓB'}
   compSectionFunctor : Section F Dᴰ → (G : Functor B C) → Section (F ∘F G) Dᴰ
   compSectionFunctor Fᴰ G .F-obᴰ d     = Fᴰ .F-obᴰ (G .F-ob d)
   compSectionFunctor Fᴰ G .F-homᴰ f    = Fᴰ .F-homᴰ (G .F-hom f)
-  compSectionFunctor Fᴰ G .F-idᴰ       = R.≡[]-rectify (R.≡[]∙ _ _
-    (cong (Fᴰ .F-homᴰ) (G .F-id))
-    (Fᴰ .F-idᴰ))
-  compSectionFunctor Fᴰ G .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _
-    (cong (Fᴰ .F-homᴰ) (G .F-seq f g))
-    (Fᴰ .F-seqᴰ (G .F-hom f) (G .F-hom g)))
+  compSectionFunctor Fᴰ G .F-idᴰ       = R.rectify $ R.≡out $
+      R.≡in (cong (Fᴰ .F-homᴰ) (G .F-id))
+    ∙ R.≡in (Fᴰ .F-idᴰ)
+  compSectionFunctor Fᴰ G .F-seqᴰ f g = R.rectify $ R.≡out $
+      R.≡in (cong (Fᴰ .F-homᴰ) (G .F-seq f g))
+    ∙ R.≡in (Fᴰ .F-seqᴰ (G .F-hom f) (G .F-hom g))
 
 module _ {D : Category ℓD ℓD'}
          {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
@@ -292,12 +293,12 @@ module _ {B : Category ℓB ℓB'}
   compFunctorᴰSection : Functorᴰ F Cᴰ Dᴰ → Section G Cᴰ → Section (F ∘F G) Dᴰ
   compFunctorᴰSection Fᴰ Gᴰ .F-obᴰ d    = Fᴰ .F-obᴰ (Gᴰ .F-obᴰ d)
   compFunctorᴰSection Fᴰ Gᴰ .F-homᴰ f   = Fᴰ .F-homᴰ (Gᴰ .F-homᴰ f)
-  compFunctorᴰSection Fᴰ Gᴰ .F-idᴰ      = R.≡[]-rectify (R.≡[]∙ _ _
-    (λ i → Fᴰ .F-homᴰ (Gᴰ .F-idᴰ i))
-    (Fᴰ .F-idᴰ))
-  compFunctorᴰSection Fᴰ Gᴰ .F-seqᴰ f g = R.≡[]-rectify (R.≡[]∙ _ _
-    (λ i → Fᴰ .F-homᴰ (Gᴰ .F-seqᴰ f g i))
-    (Fᴰ .F-seqᴰ (Gᴰ .F-homᴰ f) (Gᴰ .F-homᴰ g)))
+  compFunctorᴰSection Fᴰ Gᴰ .F-idᴰ      = R.rectify $ R.≡out $
+      R.≡in (congP (λ _ → Fᴰ .F-homᴰ) (Gᴰ .F-idᴰ))
+    ∙ R.≡in (Fᴰ .F-idᴰ)
+  compFunctorᴰSection Fᴰ Gᴰ .F-seqᴰ f g = R.rectify $ R.≡out $
+      R.≡in (congP (λ _ → Fᴰ .F-homᴰ) (Gᴰ .F-seqᴰ f g))
+    ∙ R.≡in (Fᴰ .F-seqᴰ (Gᴰ .F-homᴰ f) (Gᴰ .F-homᴰ g))
 
 module _ {C : Category ℓC ℓC'}
          {D : Category ℓD ℓD'}