Adapt proofs to new displayed category reasoning.

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ᴰ))
 

Cubical/Categories/Displayed/Cartesian.agda

@@ -149,73 +149,54 @@ 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ᴰ
 
       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

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'}

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'}