Pullback.idr

Definition

Spans in a category is a pair of morphisms pointing to a common apex

public export
record Span {0 o : Type} {c : Category o} where
  constructor MkSpan
  o1, o2, apex : o
  f : o1 ~> apex
  g : o2 ~> apex

definition A Cone of a span is a pair of morphisms from a common “tip” to each “leg” of the span such that the induced triangles commute.

public export
record Cone {0 o : Type} {c : Category o} (0 s : Span {o, c}) (tip : o) where
  constructor MkCone
  q_1 : tip ~> s.o1
  q_2 : tip ~> s.o2
  commutes : (q_1 |> s.f) {a = tip, b = s.o1, c = s.apex} === (q_2 |> s.g) {a = tip, b = s.o2, c = s.apex}

> [!definition]
> 
> In a category $\cat{C}$, given morphisms $f : C(X, Z)$ and $g : C(Y, Z)$, the pullback
> is a triple $A ∈ \cat{C}$, $p_1 : C(A, X)$, $\p_2 : C(A, Y)$ such that the square
> $p_1 ; f = p_2 ; g$ commutes, and that for any other triple $(A' ∈ \cat{C}, q_1 : C(A', X), q_2 : C(A', Y))$
> we have a unique morphism $u : C(A', A)$ such that the triangles $u ; p_2 = q_2$, $u ; p_1 = q_1$ commute.
> 
> ```haskell
> public export
> record Pullback {0 o : Type} {c : Category o} (s : Span {o, c}) where
>   constructor MkPullback
>   0 p : o
>   p_1 : p ~> s.o1
>   p_2 : p ~> s.o2
>   0 square : (p_1 |> s.f) {a = p, b = s.o1, c = s.apex} ===
>              (p_2 |> s.g) {a = p, b = s.o2, c = s.apex}
>   prop_inverse : (x : o) -> Cone s x -> x ~> p
>   0 inverses : let
>     0 prop : (x : o) -> x ~> p -> Cone s x
>     prop x m = MkCone (m |> p_1) (m |> p_2) (trans (sym $ c.compAssoc ? ? ? ? m p_1 s.f) $
>                                              trans (cong ((|:>) c m) square) (c.compAssoc ? ? ? ? m p_2 s.g) )
>     in (x : o) -> ((cone : Cone s x) -> prop x (prop_inverse x cone) === cone)
>                 * ((mor : x ~> p) -> prop_inverse x (prop x mor) === mor)
> ```


We implement the universal property as a bijection proof because proving uniqueness via contradiction is
sometimes difficult in Idris. Bijections between morphisms are still tough but a lot more reliable.

Here we show how the type $Σ (x : a) (y : b) . f(x) == g(y)$ is a pullback in set

```haskell
SigmaPullback : {a, b, c : Type} -> (f : a -> c) -> (g : b -> c) -> Pullback {c = Set} (MkSpan a b c f g)
SigmaPullback f g = MkPullback
    (Σ (x : a) | Σ (y : b) | f x === g y)
    π1
    (.π2.π1)
    (funExt $ \v => v.π2.π2)
    (\xty , cn, vx => cn.q_1 vx ## cn.q_2 vx ## app cn.commutes vx)
    (\vx => (\(MkCone q1 q2 sq) => cong (MkCone q1 q2) (UIP _ _))
         && (let
                 fnProof : (xx : vx -> Σ a (\x => Σ b (\y => f x = g y))) ->
                   (vy : vx) ->
                   ((xx vy) .π1 ## (((xx vy) .π2) .π1 ## app (trans Refl (trans (cong (\g, x => g (xx x)) (funExt (\v => (v .π2) .π2))) Refl)) vy)) = xx vy
                 fnProof xx vy with (xx vy) proof pq
                   fnProof xx vy | (p1 ## p2 ## p3) = cong ((p1 ##) . (p2 ##)) (UIP _ _)
              in \xx => funExt $ \yy => fnProof xx yy))
```