Equational reasoning in a displayed category is extremely slow

[TOTBWF]

Consider the following contrived example:

module Slow
  {o ℓ o' ℓ'}
  {B : Precategory o ℓ}
  (E : Displayed B o' ℓ')
  where
  open Cat.Displayed.Reasoning E
  open Displayed E


  slow : ∀ {x} {x' : Ob[ x ]} → id' {x} {x'} ≡[ {!!} ] id'
  slow = cast[] $
    id' ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    {!!} ≡[ {!!} ]⟨ {!!} ⟩
    id' ∎

This takes Agda a good couple of seconds to load, and the goals generated give a good hint why:

?0 : Precategory.id B ≡ Precategory.id B
?1
  : Precategory.id B ≡
    (?2 ∙
     (λ i →
        (?4 ∙
         (λ i₁ →
            (?6 ∙
             (λ i₂ →
                (?8 ∙
                 (λ i₃ → (?10 ∙ (λ i₄ → (?12 ∙ (λ i₅ → Precategory.id B)) i₄)) i₃))
                i₂))
            i₁))
        i))
    i0
?2
  : _f_183 ≡
    (?4 ∙
     (λ i →
        (?6 ∙
         (λ i₁ →
            (?8 ∙
             (λ i₂ → (?10 ∙ (λ i₃ → (?12 ∙ (λ i₄ → Precategory.id B)) i₃)) i₂))
            i₁))
        i))
    i0
?3 : Hom[ _f_183 ] x' x'
?4
  : _f_195 ≡
    (?6 ∙
     (λ i →
        (?8 ∙
         (λ i₁ → (?10 ∙ (λ i₂ → (?12 ∙ (λ i₃ → Precategory.id B)) i₂)) i₁))
        i))
    i0
?5 : Hom[ _f_195 ] x' x'
?6
  : _f_207 ≡
    (?8 ∙
     (λ i → (?10 ∙ (λ i₁ → (?12 ∙ (λ i₂ → Precategory.id B)) i₁)) i))
    i0
?7 : Hom[ _f_207 ] x' x'
?8
  : _f_219 ≡ (?10 ∙ (λ i → (?12 ∙ (λ i₁ → Precategory.id B)) i)) i0
?9 : Hom[ _f_219 ] x' x'
?10 : _f_231 ≡ (?12 ∙ (λ i → Precategory.id B)) i0
?11 : Hom[ _f_231 ] x' x'
?12 : _f_243 ≡ Precategory.id B
?13 : Hom[ _f_243 ] x' x'
?14 : _g'_237 ≡[ ?12 ] id'
?15 : _g'_225 ≡[ ?10 ] _g'_237
?16 : _g'_213 ≡[ ?8 ] _g'_225
?17 : _g'_201 ≡[ ?6 ] _g'_213
?18 : _g'_189 ≡[ ?4 ] _g'_201
?19 : _g'_177 ≡[ ?2 ] _g'_189
?20 : id' ≡[ ?1 ] _g'_177

If we look at the type of the equational reasoning combinators, it's pretty clear where this quadratic buildup comes from:

  ≡[-]⟨⟩-syntax : ∀ {a b x y} {f g h : Hom a b} (p : f ≡ g) {q : g ≡ h}
               → (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
               → g' ≡[ q ] h' → f' ≡[ p ] g' → f' ≡[ p ∙ q ] h'
  ≡[-]⟨⟩-syntax f' p q' p' = p' ∙[] q'
  syntax ≡[-]⟨⟩-syntax p f' q' p' = f' ≡[ p ]⟨ p' ⟩ q'

Every time we compose, we build a composite; uh-oh! We could do a bit better here by using something like

≡[-]⟨⟩-syntax
  : ∀ {a b x y} {f g h : Hom a b}
  → (f' : Hom[ f ] x y) {g' : Hom[ g ] x y} {h' : Hom[ h ] x y}
  → (p : f ≡ g) {r : f ≡ h}
  → g' ≡[ sym p ∙ r ] h' → f' ≡[ p ] g' → f' ≡[ r ] h'
≡[-]⟨⟩-syntax f' {h' = h'} p {r = r} q' p' =
  coe0→1 (λ i → f' ≡[ Hom-set _ _ _ _ (p ∙ sym p ∙ r) r i ] h') (p' ∙[] q')

This removes the need for a cast[], but still has a quadratic buildup.

[plt-amy]

I think we can come up with a better syntax for https://github.com/agda/cubical/pull/1153?

[TOTBWF]

Will take a look again at this: seems like a nice opportunity to clean up the mess that is Cat.Displayed.Reasoning.

[TOTBWF]

Have some draft code up at https://github.com/the1lab/1lab/blob/displayed-reasoning/src/Cat/Displayed/Reasoning.lagda.md but I don't exactly love the ergonomics. Being able to re-use the reasoning combinators is pretty sweet and it does feel much snappier, so this is definitely worth pursuing further.

OTOH, the goals do get a lot worse to read: there's a lot of total-hom junk that you have to sift through constantly and C-c C-s will often solve goals as total-hom foo bar .preserves in equational reasoning blocks. We could mitigate this a bit by using a variant of Total-hom that makes the map in B implicit, but this feels bad.

[plt-amy]

while we're at it, do we have a need for total-hom over sigma? i don't like it— i also think we should get rid of the named record contractors in general fwiw

[TOTBWF]

IIRC the reason I went with a record in the first place was to use no-eta-equality, but this ended up causing quite a bit of trouble. I think we could replace it with a sigma: the only thing that could potentially cause a problem would be instances, but I don't believe that there are any that will cause trouble (aside from a dubious Inductive instance in the branch I linked 😛). I also hate preserves: one of my worst names to date and I wince every time I type it.

Replacing Total-hom with a sigma should also let us define a lot of the displayed reasoning machinery generically over sigmas. This should be useful for other displayed algebraic structures. Seems like a good idea all around: I'll open an issue for it and give it a go.