Library UniMath.CategoryTheory.limits.pushouts

Direct implementation of pushouts
Definition of Epi in terms of a pushout diagram
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.TransportMorphisms.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.coequalizers.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Core.Functors.

Local Open Scope cat.

Section def_po.

  Context {C : category}.

  Definition isPushout {a b c d : C} (f : a --> b) (g : a --> c)
             (in1 : b --> d) (in2 : c --> d) (H : f · in1 = g · in2) : UU :=
    ∏ e (h : b --> e) (k : c --> e) (H : f · h = g · k),
    ∃! hk : d --> e, (in1 · hk = h) × (in2 · hk = k).

  Lemma isaprop_isPushout {a b c d : C} (f : a --> b) (g : a --> c)
        (in1 : b --> d) (in2 : c --> d) (H : f · in1 = g · in2) :
    isaprop (isPushout f g in1 in2 H).
  Show proof.
    repeat (apply impred; intro).
    apply isapropiscontr.

  Lemma PushoutArrowUnique {a b c d : C} (f : a --> b) (g : a --> c)
        (in1 : b --> d) (in2 : c --> d) (H : f · in1 = g · in2)
        (P : isPushout f g in1 in2 H) e (h : b --> e) (k : c --> e)
        (Hcomm : f · h = g · k)
        (w : d --> e)
        (H1 : in1 · w = h) (H2 : in2 · w = k) :
    w = (pr1 (pr1 (P e h k Hcomm))).
  Show proof.
    set (T := tpair (fun hk : d --> e => dirprod (in1 · hk = h)(in2 · hk = k))
                    w (make_dirprod H1 H2)).
    set (T' := pr2 (P e h k Hcomm) T).
    exact (base_paths _ _ T').

  Definition Pushout {a b c : C} (f : a --> b) (g : a --> c) :=
    ∑ pfg : (∑ p : C, (b --> p) × (c --> p)),
      ∑ H : f · pr1 (pr2 pfg) = g · pr2 (pr2 pfg),
        isPushout f g (pr1 (pr2 pfg)) (pr2 (pr2 pfg)) H.

  Definition Pushouts : UU :=
     ∏ (a b c : C) (f : a --> b) (g : a --> c), Pushout f g.

  Definition hasPushouts : UU :=
    ∏ (a b c : C) (f : a --> b) (g : a --> c), ishinh (Pushout f g).

  Definition PushoutObject {a b c : C} {f : a --> b} {g : a --> c}:
    Pushout f g -> C := λ H, pr1 (pr1 H).
  Coercion PushoutObject : Pushout >-> ob.

  Definition PushoutIn1 {a b c : C} {f : a --> b} {g : a --> c}
             (Pb : Pushout f g) : b --> Pb := pr1 (pr2 (pr1 Pb)).

  Definition PushoutIn2 {a b c : C} {f : a --> b} {g : a --> c}
             (Pb : Pushout f g) : c --> Pb := pr2 (pr2 (pr1 Pb)).

  Definition PushoutSqrCommutes {a b c : C} {f : a --> b} {g : a --> c}
             (Pb : Pushout f g) :
    f · PushoutIn1 Pb = g · PushoutIn2 Pb.
  Show proof.
    exact (pr1 (pr2 Pb)).

  Definition isPushout_Pushout {a b c : C} {f : a --> b} {g : a --> c}
             (P : Pushout f g) :
    isPushout f g (PushoutIn1 P) (PushoutIn2 P) (PushoutSqrCommutes P).
  Show proof.
    exact (pr2 (pr2 P)).

  Definition PushoutArrow {a b c : C} {f : a --> b} {g : a --> c}
             (Pb : Pushout f g) e (h : b --> e) (k : c --> e)
             (H : f · h = g · k) :
    Pb --> e := pr1 (pr1 (isPushout_Pushout Pb e h k H)).

  Lemma PushoutArrow_PushoutIn1 {a b c : C} {f : a --> b} {g : a --> c}
        (Pb : Pushout f g) e (h : b --> e) (k : c --> e)
        (H : f · h = g · k) :
    PushoutIn1 Pb · PushoutArrow Pb e h k H = h.
  Show proof.
    exact (pr1 (pr2 (pr1 (isPushout_Pushout Pb e h k H)))).

  Lemma PushoutArrow_PushoutIn2 {a b c : C} {f : a --> b} {g : a --> c}
        (Pb : Pushout f g) e (h : b --> e) (k : c --> e)
        (H : f · h = g · k) :
    PushoutIn2 Pb · PushoutArrow Pb e h k H = k.
  Show proof.
    exact (pr2 (pr2 (pr1 (isPushout_Pushout Pb e h k H)))).

  Definition make_Pushout {a b c : C} (f : C⟦a, b⟧) (g : C⟦a, c⟧)
             (d : C) (in1 : C⟦b,d⟧) (in2 : C ⟦c,d⟧)
             (H : f · in1 = g · in2)
             (ispb : isPushout f g in1 in2 H)
    : Pushout f g.
  Show proof.
    use tpair.
    - use tpair.
      + apply d.
      + exists in1.
        exact in2.
    - exists H.
      apply ispb.

  Definition make_isPushout {a b c d : C} (f : C ⟦a, b⟧) (g : C ⟦a, c⟧)
             (in1 : C⟦b,d⟧) (in2 : C⟦c,d⟧) (H : f · in1 = g · in2) :
    (∏ e (h : C ⟦b, e⟧) (k : C⟦c,e⟧)(Hk : f · h = g · k),
        ∃! hk : C⟦d,e⟧,(in1 · hk = h) × (in2 · hk = k)) →
    isPushout f g in1 in2 H.
  Show proof.
    intros H' x cx k sqr.
    apply H'. assumption.

  Lemma MorphismsOutofPushoutEqual {a b c d : C} {f : a --> b} {g : a --> c}
        {in1 : b --> d} {in2 : c --> d} {H : f · in1 = g · in2}
        (P : isPushout f g in1 in2 H) {e}
        (w w': d --> e)
        (H1 : in1 · w = in1 · w') (H2 : in2 · w = in2 · w')
    : w = w'.
  Show proof.
    assert (Hw : f · in1 · w = g · in2 · w).
    { rewrite H. apply idpath. }
    assert (Hw' : f · in1 · w' = g · in2 · w').
    { rewrite H. apply idpath. }
    set (Pb := make_Pushout _ _ _ _ _ _ P).
    rewrite <- assoc in Hw. rewrite <- assoc in Hw.
    set (Xw := PushoutArrow Pb e (in1 · w) (in2 · w) Hw).
    intermediate_path Xw; [ apply PushoutArrowUnique; apply idpath |].
    apply pathsinv0.
    apply PushoutArrowUnique. apply pathsinv0. apply H1.
    apply pathsinv0. apply H2.

  Definition identity_is_Pushout_input {a b c : C} {f : a --> b} {g : a --> c}
             (Pb : Pushout f g) :
    ∑ hk : Pb --> Pb,
      (PushoutIn1 Pb · hk = PushoutIn1 Pb) × (PushoutIn2 Pb · hk = PushoutIn2 Pb).
  Show proof.
    exists (identity Pb).
    apply make_dirprod; apply id_right.

  Lemma PushoutEndo_is_identity {a b c : C} {f : a --> b} {g : a --> c}
        (Pb : Pushout f g) (k : Pb --> Pb)
        (kH1 : PushoutIn1 Pb · k = PushoutIn1 Pb)
        (kH2 : PushoutIn2 Pb · k = PushoutIn2 Pb) :
    identity Pb = k.
  Show proof.
    set (H1 := tpair ((fun hk : Pb --> Pb => dirprod (_ · hk = _)(_ · hk = _)))
                     k (make_dirprod kH1 kH2)).
    assert (H2 : identity_is_Pushout_input Pb = H1).
    - apply proofirrelevancecontr.
      apply (isPushout_Pushout Pb).
      apply PushoutSqrCommutes.
    - apply (base_paths _ _ H2).

  Definition from_Pushout_to_Pushout {a b c : C} {f : a --> b} {g : a --> c}
             (Pb Pb': Pushout f g) : Pb --> Pb'.
  Show proof.
    apply (PushoutArrow Pb Pb' (PushoutIn1 _ ) (PushoutIn2 _)).
    exact (PushoutSqrCommutes _ ).

  Lemma are_inverses_from_Pushout_to_Pushout {a b c : C} {f : a --> b}
        {g : a --> c} (Pb Pb': Pushout f g) :
    is_inverse_in_precat (from_Pushout_to_Pushout Pb' Pb)
                         (from_Pushout_to_Pushout Pb Pb').
  Show proof.
    split.

First identity
    apply pathsinv0.
    apply PushoutEndo_is_identity.
    unfold from_Pushout_to_Pushout.
    unfold from_Pushout_to_Pushout.
    rewrite assoc.
    rewrite PushoutArrow_PushoutIn1.
    rewrite PushoutArrow_PushoutIn1.
    apply idpath.

    unfold from_Pushout_to_Pushout.
    unfold from_Pushout_to_Pushout.
    rewrite assoc.
    rewrite PushoutArrow_PushoutIn2.
    rewrite PushoutArrow_PushoutIn2.
    apply idpath.

Second identity
    apply pathsinv0.
    apply PushoutEndo_is_identity.
    unfold from_Pushout_to_Pushout.
    unfold from_Pushout_to_Pushout.
    rewrite assoc.
    rewrite PushoutArrow_PushoutIn1.
    rewrite PushoutArrow_PushoutIn1.
    apply idpath.

    unfold from_Pushout_to_Pushout.
    unfold from_Pushout_to_Pushout.
    rewrite assoc.
    rewrite PushoutArrow_PushoutIn2.
    rewrite PushoutArrow_PushoutIn2.
    apply idpath.

  Lemma isziso_from_Pushout_to_Pushout {a b c : C} {f : a --> b} {g : a --> c}
        (Pb Pb': Pushout f g) :
    is_z_isomorphism (from_Pushout_to_Pushout Pb Pb').
  Show proof.
    exists (from_Pushout_to_Pushout Pb' Pb).
    apply are_inverses_from_Pushout_to_Pushout.

  Definition z_iso_from_Pushout_to_Pushout {a b c : C} {f : a --> b} {g : a --> c}
             (Pb Pb': Pushout f g) : z_iso Pb Pb' :=
    tpair _ _ (isziso_from_Pushout_to_Pushout Pb Pb').

  Lemma inv_from_z_iso_z_iso_from_Pushout (a b c : C) (f : a --> b) (g : a --> c)
        (Pb : Pushout f g) (Pb' : Pushout f g):
      inv_from_z_iso (z_iso_from_Pushout_to_Pushout Pb Pb')
      = from_Pushout_to_Pushout Pb' Pb.
  Show proof.
      apply pathsinv0.
      apply inv_z_iso_unique'.
      set (T:= are_inverses_from_Pushout_to_Pushout Pb' Pb).
      apply (pr1 T).

End def_po.

Make the C not implicit for Pushouts
Arguments Pushouts : clear implicits.

Section Universal_Unique.

  Variable C : category.
  Hypothesis H : is_univalent C.

    Lemma isaprop_Pushouts: isaprop (Pushouts C).
    Show proof.
      apply impred; intro a; apply impred; intro b; apply impred; intro c;
        apply impred; intro p1; apply impred; intro p2;
          apply invproofirrelevance.
      intros Pb Pb'.
      apply subtypePath.
      - intro; apply isofhleveltotal2.
        + apply C.
        + intros; apply isaprop_isPushout.
      - apply (total2_paths_f
                 (isotoid _ H (z_iso_from_Pushout_to_Pushout Pb Pb' ))).
        rewrite transportf_dirprod, transportf_isotoid', transportf_isotoid'.
        fold (PushoutIn1 Pb). fold (PushoutIn2 Pb).
        use (dirprodeq); simpl.

        destruct Pb as [Cone bla];
          destruct Pb' as [Cone' bla'];
          simpl in *.

        destruct Cone as [p [h k]];
          destruct Cone' as [p' [h' k']];
          simpl in *.

        unfold from_Pushout_to_Pushout.
        rewrite PushoutArrow_PushoutIn1.
        apply idpath.

        unfold from_Pushout_to_Pushout.
        rewrite PushoutArrow_PushoutIn2.
        apply idpath.

End Universal_Unique.

In this section we prove that the pushout of an epimorphism is an epimorphism.
Section epi_po.

  Variable C : category.

The pushout of an epimorphism is an epimorphism.
  Lemma EpiPushoutisEpi {a b c : C} (E : Epi _ a b) (g : a --> c) (PB : Pushout E g) :
    isEpi (PushoutIn2 PB).
  Show proof.
    apply make_isEpi. intros z g0 h X.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout PB) _ _ _ X).

    set (X0 := maponpaths (λ f, g · f) X); simpl in X0.
    rewrite assoc in X0. rewrite assoc in X0.
    rewrite <- (PushoutSqrCommutes PB) in X0.
    rewrite <- assoc in X0. rewrite <- assoc in X0.
    apply (pr2 E _ _ _) in X0. apply X0.

Same result for the other morphism
  Lemma EpiPushoutisEpi' {a b c : C} (f : a --> b) (E : Epi _ a c) (PB : Pushout f E) :
    isEpi (PushoutIn1 PB).
  Show proof.
    apply make_isEpi. intros z g0 h X.
    use (MorphismsOutofPushoutEqual (isPushout_Pushout PB) _ _ X).

    set (X0 := maponpaths (λ f', f · f') X); simpl in X0.
    rewrite assoc in X0. rewrite assoc in X0.
    rewrite (PushoutSqrCommutes PB) in X0.
    rewrite <- assoc in X0. rewrite <- assoc in X0.
    apply (pr2 E _ _ _) in X0. apply X0.

End epi_po.

Criteria for existence of pushouts.
Section po_criteria.

  Variable C : category.

  Definition Pushout_from_Coequalizer_BinCoproduct_eq (X Y Z : C)
             (f : Z --> X) (g : Z --> Y) (BinCoprod : BinCoproduct X Y)
             (CEq : Coequalizer (f · (BinCoproductIn1 BinCoprod))
                                (g · (BinCoproductIn2 BinCoprod))) :
    f · ((BinCoproductIn1 BinCoprod) · CoequalizerArrow CEq)
    = g · ((BinCoproductIn2 BinCoprod) · CoequalizerArrow CEq).
  Show proof.
    repeat rewrite assoc. apply CoequalizerEqAr.

  Definition Pushout_from_Coequalizer_BinCoproduct_isPushout (X Y Z : C)
             (f : Z --> X) (g : Z --> Y) (BinCoprod : BinCoproduct X Y)
             (CEq : Coequalizer (f · (BinCoproductIn1 BinCoprod))
                                (g · (BinCoproductIn2 BinCoprod))) :
    isPushout f g (BinCoproductIn1 BinCoprod · CoequalizerArrow CEq)
               (BinCoproductIn2 BinCoprod · CoequalizerArrow CEq)
               (Pushout_from_Coequalizer_BinCoproduct_eq
                  X Y Z f g BinCoprod CEq).
  Show proof.
    use make_isPushout.
    intros e h k Hk.
    set (com1 := BinCoproductIn1Commutes C _ _ BinCoprod _ h k).
    set (com2 := BinCoproductIn2Commutes C _ _ BinCoprod _ h k).
    apply (maponpaths (λ l : _, f · l)) in com1.
    apply (maponpaths (λ l : _, g · l)) in com2.
    rewrite <- com1 in Hk. rewrite <- com2 in Hk.
    repeat rewrite assoc in Hk.
    apply (unique_exists (CoequalizerOut CEq _ _ Hk)).

    split.
    rewrite <- assoc. rewrite (CoequalizerCommutes CEq e _).
    exact (BinCoproductIn1Commutes C _ _ BinCoprod _ h k).
    rewrite <- assoc. rewrite (CoequalizerCommutes CEq e _).
    exact (BinCoproductIn2Commutes C _ _ BinCoprod _ h k).

    intros y. apply isapropdirprod. apply C. apply C.

    intros y H. induction H as [t p]. apply CoequalizerOutsEq.
    apply BinCoproductArrowsEq.
    rewrite <- assoc in t. rewrite t.
    rewrite (CoequalizerCommutes CEq e _). apply pathsinv0.
    exact (BinCoproductIn1Commutes C _ _ BinCoprod _ h k).
    rewrite <- assoc in p. rewrite p.
    rewrite (CoequalizerCommutes CEq e _). apply pathsinv0.
    exact (BinCoproductIn2Commutes C _ _ BinCoprod _ h k).

  Definition Pushout_from_Coequalizer_BinCoproduct (X Y Z : C)
             (f : Z --> X) (g : Z --> Y) (BinCoprod : BinCoproduct X Y)
             (CEq : Coequalizer (f · (BinCoproductIn1 BinCoprod))
                                (g · (BinCoproductIn2 BinCoprod))) :
    Pushout f g.
  Show proof.
    use (make_Pushout f g CEq ((BinCoproductIn1 BinCoprod)
                               · CoequalizerArrow CEq)
                    ((BinCoproductIn2 BinCoprod) · CoequalizerArrow CEq)).
    - apply Pushout_from_Coequalizer_BinCoproduct_eq.
    - apply Pushout_from_Coequalizer_BinCoproduct_isPushout.

  Definition Pushouts_from_Coequalizers_BinCoproducts
             (BinCoprods : BinCoproducts C)
             (CEqs : Coequalizers C) : Pushouts C.
  Show proof.
    intros Z X Y f g.
    use (Pushout_from_Coequalizer_BinCoproduct X Y Z f g).
    apply BinCoprods.
    apply CEqs.
End po_criteria.

Section lemmas_on_pushouts.

  Context {C : category}.
  Context {a b c d : C}.
  Context {f : C ⟦a, b⟧} {g : C ⟦a, c⟧} {h : C⟦b, d⟧} {k : C⟦c, d⟧}.
  Variable H : f · h = g · k.

Pushout is symmetric, i.e., we can rotate a po square

  Lemma is_symmetric_isPushout : isPushout _ _ _ _ H -> isPushout _ _ _ _ (!H).
  Show proof.
    intro isPo.
    set (Po := make_Pushout _ _ _ _ _ _ isPo).
    use make_isPushout.
    intros e x y Hxy.
    use unique_exists.
    - use (PushoutArrow Po).
      + exact y.
      + exact x.
      + exact (! Hxy).
    - cbn. split.
      + apply (PushoutArrow_PushoutIn2 Po).
      + apply (PushoutArrow_PushoutIn1 Po).
    - intros y0. apply isapropdirprod.
      + apply C.
      + apply C.
    - intros y0. intros X. cbn in X.
      use PushoutArrowUnique.
      + exact (dirprod_pr2 X).
      + exact (dirprod_pr1 X).

End lemmas_on_pushouts.

Section pushout_up_to_z_iso.

  Context {C : category}.

  Local Lemma isPushout_up_to_z_iso_eq {a a' b c d : C} (f : a --> b) (g : a --> c)
        (in1 : b --> d) (in2 : c --> d) (H : f · in1 = g · in2) (i : z_iso a' a) :
    i · f · in1 = i · g · in2.
  Show proof.
    rewrite <- assoc. rewrite <- assoc. rewrite H. apply idpath.

  Lemma isPushout_up_to_z_iso {a a' b c d : C} (f : a --> b) (g : a --> c)
        (in1 : b --> d) (in2 : c --> d) (H : f · in1 = g · in2) (i : z_iso a' a)
        (iPo : isPushout (i · f) (i · g) in1 in2 (isPushout_up_to_z_iso_eq f g in1 in2 H i)) :
    isPushout f g in1 in2 H.
  Show proof.
    set (Po := make_Pushout _ _ _ _ _ _ iPo).
    use make_isPushout.
    intros e h k Hk.
    use unique_exists.
    - use (PushoutArrow Po).
      + exact h.
      + exact k.
      + use isPushout_up_to_z_iso_eq. exact Hk.
    - cbn. split.
      + exact (PushoutArrow_PushoutIn1 Po e h k (isPushout_up_to_z_iso_eq f g h k Hk i)).
      + exact (PushoutArrow_PushoutIn2 Po e h k (isPushout_up_to_z_iso_eq f g h k Hk i)).
    - intros y. apply isapropdirprod.
      + apply C.
      + apply C.
    - intros y X. cbn in X.
      use PushoutArrowUnique.
      + exact (dirprod_pr1 X).
      + exact (dirprod_pr2 X).

End pushout_up_to_z_iso.

Section pushout_paths.

  Context {C : category}.

  Lemma isPushout_mor_paths {a b c d : C} {f1 f2 : a --> b} {g1 g2 : a --> c} {in11 in21 : b --> d}
        {in12 in22 : c --> d} (e1 : f1 = f2) (e2 : g1 = g2) (e3 : in11 = in21) (e4 : in12 = in22)
        (H1 : f1 · in11 = g1 · in12) (H2 : f2 · in21 = g2 · in22)
        (iPo : isPushout f1 g1 in11 in12 H1) : isPushout f2 g2 in21 in22 H2.
  Show proof.
    induction e1, e2, e3, e4.
    assert (e5 : H1 = H2) by apply C.
    induction e5.
    exact iPo.

End pushout_paths.

Proof that f: A -> B is an epi is the same as saying that the diagram 
A ---> B
|      |
|      |  id
‌v     ‌‌ v
B----> B
  id
is a pushout
Section EpiPushoutId.

  Context {C : category} {A B : C} (f : C⟦A,B ⟧).

  Lemma epi_to_pushout : isEpi f -> isPushout f f (identity _) (identity _) (idpath _).
  Show proof.
    intro h.
    red.
    intros x p1 p2 eqx.
    assert (hp : p1 = p2).
    { now apply h. }
    induction hp.
    apply (unique_exists p1).
    - split; apply id_left.
    - intros y. apply isapropdirprod; apply homset_property.
    - intros y [h1 _].
      now rewrite id_left in h1.

  Lemma pushout_to_epi : isPushout f f (identity _) (identity _) (idpath _)
                          -> isEpi f.
  Show proof.
    intros hf.
    intros D p1 p2 hp.
    apply hf in hp.
    destruct hp as [[p [hp1 hp2]] _].
    now rewrite <- hp1,hp2.

End EpiPushoutId.

Lemma induced_precategory_reflects_pushouts {M : category} {X : Type} (j : X -> ob M)
      {a b c d : induced_category M j}
      (f : b <-- a) (g : c <-- a) (p1 : d <-- b) (p2 : d <-- c)
      (H : p1 ∘ f = p2 ∘ g) :
  isPushout (# (induced_precategory_incl j) f)
            (# (induced_precategory_incl j) g)
            (# (induced_precategory_incl j) p1)
            (# (induced_precategory_incl j) p2) H ->
  isPushout f g p1 p2 H.
Show proof.
  exact (λ pb T, pb (j T)).