Rework displayed category reasoning.

This new technique is both more performant, more readable and reduces
boilerplate.

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 _∘_
 

Cubical/Categories/Displayed/Reasoning.agda

@@ -1,11 +1,30 @@
+{-
+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
 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 _ _ _ _)