Banish `Total-hom` in favor of a sigma type

[TOTBWF]

As noted in #463, Total-hom is a bit of a wart, and makes any solution for displayed reasoning non-modular. Moreover, the names are pretty bad! Replacing it with a sigma type seems like a good move all around.

[TOTBWF]

Ok, there is one catch. We do have an instance that uses Total-hom in a non-trivial way in Cat.Displayed.Univalence.Thin:

  instance
    Extensional-Hom
      : ∀ {a b ℓr} ⦃ sa : Extensional (⌞ a ⌟ → ⌞ b ⌟) ℓr ⦄
      → Extensional (So.Hom a b) ℓr
    Extensional-Hom ⦃ sa ⦄ = injection→extensional!
      (Structured-hom-path spec) sa

This is actually a pretty important instance: it's how extensionality kicks in for things like group homomorphisms.

We can't convert this to an instance like

  Extensional-Σ-prop
    : ∀ {ℓ ℓ' ℓr} {A : Type ℓ} {B : A → Prop ℓ'}
    → ⦃ ea : Extensional A ℓr ⦄ → Extensional (Σ A λ x → ∣ B x ∣) ℓr
  Extensional-Σ-prop ⦃ ea ⦄ = Σ-prop-extensional (λ x → hlevel 1) ea

because Agda will never be able to solve for the is-tr portion of the B family.

I see two possible solutions. The obvious option is to add a bunch of concrete instances for sigmas over things like is-group-hom, but this seems sub-optimal. Alternatively, we could add a separate worker class for doing extensionality in sigma-like things, but this is straying dangerously close to ExtensionalityP.

[TOTBWF]

There are also some places where inference gets much worse. Consider the following code from Algebra.Group.Cat.FinitelyComplete

Direct-product : Group ℓ → Group ℓ → Group ℓ
Direct-product (G , Gg) (H , Hg) = to-group G×Hg where
  module G = Group-on Gg
  module H = Group-on Hg

  G×Hg : make-group (∣ G ∣ × ∣ H ∣)
  G×Hg .make-group.group-is-set = hlevel 2
  G×Hg .make-group.unit = G.unit , H.unit
  G×Hg .make-group.mul (a , x) (b , y) = a G.⋆ b , x H.⋆ y
  G×Hg .make-group.inv (a , x) = a G.⁻¹ , x H.⁻¹
  G×Hg .make-group.assoc x y z = ap₂ _,_ G.associative H.associative
  G×Hg .make-group.invl x = ap₂ _,_ G.inversel H.inversel
  G×Hg .make-group.idl x = ap₂ _,_ G.idl H.idl

proj₁ : Groups.Hom (Direct-product G H) G
proj₁ .fst = fst
proj₁ .snd .pres-⋆ x y = refl

proj₂ : Groups.Hom (Direct-product G H) H
proj₂ .fst = snd
proj₂ .snd .pres-⋆ x y = refl

factor : Groups.Hom G H → Groups.Hom G K → Groups.Hom G (Direct-product H K)
factor f g .fst x = f · x , g · x
factor f g .snd .pres-⋆ x y = ap₂ _,_ (f .snd .pres-⋆ _ _) (g .snd .pres-⋆ _ _)

Direct-product-is-product : is-product (Groups ℓ) {G} {H} proj₁ proj₂
Direct-product-is-product = ?

When we used Total-hom, we actually stored the Sets G, H inside of the telescope of Total-hom. This is no longer the case with a sigma, which results in a shocking amount of yellow:

_P.fst_434 : Set ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.29-57 ]
_G.fst_435 : Set ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_436 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_437 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_438 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_439 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_H.fst_440 : Set ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]
_441
  : Precategory.Hom (Groups ℓ)
    (_P.fst_434 ,
     Direct-product (_G.fst_435 , G .snd) (_H.fst_440 , H .snd) .snd)
    G  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.59-64 ]
_442 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]
_443 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]
_444 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]
_445 : Type ℓ  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]
_450
  : Precategory.Hom (Groups ℓ)
    (_P.fst_434 ,
     Direct-product (_G.fst_435 , G .snd) (_H.fst_440 , H .snd) .snd)
    H  [ at /Users/reedmullanix/Documents/Projects/1lab/src/Algebra/Group/Cat/FinitelyComplete.lagda.md:130.65-70 ]

———— Error —————————————————————————————————————————————————
error: [UnsolvedConstraints]
Failed to solve the following constraints:
  ∣ _H.fst_440 ∣ = ∣ H .fst ∣ : Type ℓ (blocked on _H.fst_440)
  ∣ _H.fst_440 ∣ = ∣ H .fst ∣ (blocked on _H.fst_440)
  ∣ _G.fst_435 ∣ = ∣ G .fst ∣ : Type ℓ (blocked on _G.fst_435)
  ∣ _G.fst_435 ∣ = ∣ G .fst ∣ (blocked on _G.fst_435)
  ∣ _P.fst_434 ∣ = Σ ∣ _G.fst_435 ∣ (λ _ → ∣ _H.fst_440 ∣)
    (blocked on _P.fst_434)
  Σ ∣ _G.fst_435 ∣ (λ _ → ∣ _H.fst_440 ∣) = ∣ _P.fst_434 ∣ : Type ℓ
    (blocked on _P.fst_434)

You can solve this by filling in the implicit for P, but this feels quite bad.

[TOTBWF]

After sleeping on this, I think we can solve the problem by introducing a wrapper record around morphisms in Sets so we can retain the telescope. Definitely makes the experience crunchier, but not sure if there's a better solution.

[plt-amy]

That's probably worse than just keeping Total-hom, but maybe it should be called ∫Hom and have an anonymous constructor (and probably be an eta-equality type?). Maybe the fields could be called base and over instead?

[TOTBWF]

If all else fails then yeah, that works. I do want to try and see if there's some reasonably generic way to do this though: we are going to have to do this whole song-and-dance over again for displayed bicategories

[TOTBWF]

There are also a couple of other places where inference absolutely dies when working over Sets, so I'm not 100% convinced that wrapping is a bad idea.

As a concrete example, things like is-product (Sets l) fst snd have the same yellow problems: Agda can't find a unique solution for the Set implicits and then complains about | _A | = | A |. This owned me extremely hard when I was doing topology.