Simpler definition of span pushout

[Alizter]

When reading Blakers-Massey I noticed that we could use a more efficient implementation of SPushout. Currently, we define it as a special case of a Pushout, which is in turn a special case of Coeq, which in turn is a special case of GraphQuotient.

It's not hard to see that you can simplify this all the way through to end up with something like this:

  Definition SPushout := 
    @GraphQuotient (X + Y) (fun xy xy' => match xy, xy' with
                                        | inl x, inr y => Q x y
                                        | _, _ => Empty
                                        end).

Proving the rec/ind is also simple and modulo some changes to Freudenthal.v, it should work.

I created this issue so we can discuss the tradeoffs first. The main advantage would be the more compact term size and the main disadvantage would be pushout lemmas not being applicable to span pushouts. Interested to know what others think.

[jdchristensen]

I'm open to the idea. In the past, I've pushed for building things up in stages and reusing the work done at the previous stage, but I've seen lots of cases now where it seems better to prove things again for, say, pushouts, after already proving them for, say, coequalizers, because the work needed to translate between the two is often harder than the work in just proving things again.

That said, while SPushout isn't used much currently, David Warn's shorter type-theoretic paper on path spaces of pushouts uses that set-up, and some students in my class should be "pushing" work on that soon. I had forgotten to point out SPushout to them, but they might want to use it, in which case they'll probably need to know basic facts about it, which would need to be reproved if the definition changes. So maybe we should wait a bit to see how that plays out?

BTW, if you trace through the definition of Pushout, you'll see that it is equivalent to a very similar family, with Q x y replaced with hfiber f x * hfiber g y, and again, the other cases being sent to Empty. So we could in fact define Pushout in terms of SPushout if we wanted to, and prove the fundamental facts about SPushout, inheriting them to Pushout, instead of the other way around.

[Alizter]

That said, while SPushout isn't used much currently, David Warn's shorter type-theoretic paper on path spaces of pushouts uses that set-up, and some students in my class should be "pushing" work on that soon. I had forgotten to point out SPushout to them, but they might want to use it, in which case they'll probably need to know basic facts about it, which would need to be reproved if the definition changes. So maybe we should wait a bit to see how that plays out?

That's a good point, no trouble waiting.

BTW, if you trace through the definition of Pushout, you'll see that it is equivalent to a very similar family, with Q x y replaced with hfiber f x * hfiber g y, and again, the other cases being sent to Empty. So we could in fact define Pushout in terms of SPushout if we wanted to, and prove the fundamental facts about SPushout, inheriting them to Pushout, instead of the other way around.

This is quite interesting. I would be curious if span pushouts simplify any of the pushout proofs. For instance, functionality has a more succinct description. Compare the following:

Definition functor_spushout_homotopic {X Y Z W : Type}
  {Q : X -> Y -> Type} {Q' : Z -> W -> Type}
  {f g : X -> Z} (h : f == g)
  {i j : Y -> W} (k : i == j)
  (l : forall x y, Q x y -> Q' (f x) (i y))
  (m : forall x y, Q x y -> Q' (g x) (j y))
  (H : forall x y q,
    spglue Q' (l x y q) @ ap (spushr Q') (k y)
      = ap (spushl Q') (h x) @ spglue Q' (m x y q))
  : functor_spushout f i l == functor_spushout g j m.

Lemma functor_pushout_homotopic 
  {A B C : Type} {f : A -> B} {g : A -> C}
  {A' B' C' : Type} {f' : A' -> B'} {g' : A' -> C'}
  {h h' : A -> A'} {k k' : B -> B'} {l l' : C -> C'}
  {p : k o f == f' o h} {q : l o g == g' o h}
  {p' : k' o f == f' o h'} {q' : l' o g == g' o h'}
  (t : h == h') (u : k == k') (v : l == l')
  (i : forall a, p a @ (ap f') (t a) = u (f a) @ p' a)
  (j : forall a, q a @ (ap g') (t a) = v (g a) @ q' a)
  : functor_pushout h k l p q == functor_pushout h' k' l' p' q'.