Library UniMath.CategoryTheory.Limits.PullbackConstructions

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.

Local Open Scope cat.

1. Equalizers from pullbacks and products

Section EqualizersFromPullbackProducts.
  Context {C : category}
          (PB : Pullbacks C)
          (P : BinProducts C).

  Section EqualizerConstruction.
    Context {x y : C}
            (f g : x --> y).

    Let Δ : y --> P y y := diagonalMap' P y.
    Let φ : x --> P y y := BinProductArrow _ (P y y) f g.

    Let e : Pullback Δ φ := PB _ _ _ Δ φ.
    Let i : e --> x := PullbackPr2 e.

    Proposition equalizer_from_pb_prod_eq
      : i · f = i · g.
    Show proof.
      pose (maponpaths (λ z, z · BinProductPr1 _ _) (PullbackSqrCommutes e)) as p.
      cbn in p.
      rewrite !assoc' in p.
      unfold Δ, φ, diagonalMap' in p.
      rewrite !BinProductPr1Commutes in p.
      rewrite id_right in p.
      refine (!p @ _).
      clear p.
      pose (maponpaths (λ z, z · BinProductPr2 _ _) (PullbackSqrCommutes e)) as p.
      cbn in p.
      rewrite !assoc' in p.
      unfold Δ, φ, diagonalMap' in p.
      rewrite !BinProductPr2Commutes in p.
      rewrite id_right in p.
      exact p.

    Section UMP.
      Context {w : C}
              {h : w --> x}
              (p : h · f = h · g).

      Proposition equalizer_from_pb_prod_map_eq
        : h · f · Δ = h · φ.
      Show proof.
        unfold Δ, diagonalMap', φ.
        use BinProductArrowsEq.
        - rewrite !assoc'.
          rewrite !BinProductPr1Commutes.
          rewrite id_right.
          apply idpath.
        - rewrite !assoc'.
          rewrite !BinProductPr2Commutes.
          rewrite id_right.
          exact p.

      Proposition equalizer_from_pb_prod_unique
        : isaprop (∑ (ζ : w --> e), ζ · i = h).
      Show proof.
        use invproofirrelevance.
        intros ζ₁ ζ₂.
        use subtypePath.
        {
          intro.
          apply homset_property.
        }
        use (MorphismsIntoPullbackEqual (isPullback_Pullback e)).
        - use (diagonalMap_isMonic P y).
          rewrite !assoc'.
          etrans.
          {
            apply maponpaths.
            exact (PullbackSqrCommutes e).
          }
          rewrite !assoc.
          etrans.
          {
            apply maponpaths_2.
            exact (pr2 ζ₁).
          }
          rewrite !assoc'.
          refine (!_).
          etrans.
          {
            apply maponpaths.
            exact (PullbackSqrCommutes e).
          }
          rewrite !assoc.
          etrans.
          {
            apply maponpaths_2.
            exact (pr2 ζ₂).
          }
          apply idpath.
        - exact (pr2 ζ₁ @ !(pr2 ζ₂)).

      Definition equalizer_from_pb_prod_map
        : w --> e.
      Show proof.
        use (PullbackArrow e _ (h · f) h).
        apply equalizer_from_pb_prod_map_eq.

      Proposition equalizer_from_pb_prod_comm
        : equalizer_from_pb_prod_map · i = h.
      Show proof.
        exact (PullbackArrow_PullbackPr2 e _ (h · f) h equalizer_from_pb_prod_map_eq).
    End UMP.

    Definition equalizer_from_pb_prod
      : Equalizer f g.
    Show proof.
      use make_Equalizer.
      - exact e.
      - exact i.
      - exact equalizer_from_pb_prod_eq.
      - intros w h p.
        use iscontraprop1.
        + apply equalizer_from_pb_prod_unique.
        + refine (equalizer_from_pb_prod_map p ,, _).
          exact (equalizer_from_pb_prod_comm p).
  End EqualizerConstruction.

  Definition equalizers_from_pullbacks_prods
    : Equalizers C.
  Show proof.
    intros x y f g.
    apply equalizer_from_pb_prod.
End EqualizersFromPullbackProducts.

2. Equalizers from pullbacks and a terminal object

Definition equalizers_from_pullbacks_terminal
           {C : category}
           (PB : Pullbacks C)
           (T : Terminal C)
  : Equalizers C.
Show proof.
  use equalizers_from_pullbacks_prods.
  - exact PB.
  - exact (BinProductsFromPullbacks PB T).

3. Pullback of a product

Section PullbackProduct.
  Context {C : category}
          (PC : BinProducts C)
          (PB : Pullbacks C)
          {x₁ x₂ : C}
          (f : x₁ --> x₂)
          (y : C).

  Let xy₁ : BinProduct C x₁ y := PC x₁ y.
  Let π₁ : xy₁ --> x₁ := BinProductPr1 _ _.
  Let π₂ : xy₁ --> y := BinProductPr2 _ _.

  Let xy₂ : BinProduct C x₂ y := PC x₂ y.
  Let ρ₁ : xy₂ --> x₂ := BinProductPr1 _ _.
  Let ρ₂ : xy₂ --> y := BinProductPr2 _ _.

  Let pb : Pullback ρ₁ f := PB _ _ _ ρ₁ f.

  Definition map_from_pb_prod
    : pb --> xy₁.
  Show proof.
    use BinProductArrow.
    - exact (PullbackPr2 pb).
    - exact (PullbackPr1 pb · ρ₂).

  Definition map_to_pb_prod
    : xy₁ --> pb.
  Show proof.
    use PullbackArrow.
    - use BinProductArrow.
      + exact (π₁ · f).
      + exact π₂.
    - exact π₁.
    - abstract
        (exact (BinProductPr1Commutes _ _ _ _ _ _ _)).

  Proposition pb_prod_is_inverse
    : is_inverse_in_precat
        map_from_pb_prod
        map_to_pb_prod.
  Show proof.
    unfold map_from_pb_prod, map_to_pb_prod.
    split.
    - use (MorphismsIntoPullbackEqual (isPullback_Pullback pb)).
      + rewrite !assoc'.
        rewrite PullbackArrow_PullbackPr1.
        rewrite id_left.
        use BinProductArrowsEq.
        * rewrite !assoc'.
          rewrite BinProductPr1Commutes.
          rewrite !assoc.
          etrans.
          {
            apply maponpaths_2.
            apply BinProductPr1Commutes.
          }
          refine (!_).
          apply PullbackSqrCommutes.
        * rewrite !assoc'.
          rewrite BinProductPr2Commutes.
          apply BinProductPr2Commutes.
      + rewrite !assoc'.
        rewrite PullbackArrow_PullbackPr2.
        rewrite id_left.
        apply BinProductPr1Commutes.
    - use BinProductArrowsEq.
      + rewrite !assoc'.
        rewrite BinProductPr1Commutes.
        rewrite PullbackArrow_PullbackPr2.
        rewrite id_left.
        apply idpath.
      + rewrite !assoc'.
        rewrite BinProductPr2Commutes.
        rewrite !assoc.
        rewrite PullbackArrow_PullbackPr1.
        rewrite id_left.
        apply BinProductPr2Commutes.

  Definition pb_prod_z_iso
    : z_iso pb xy₁.
  Show proof.
    use make_z_iso.
    - exact map_from_pb_prod.
    - exact map_to_pb_prod.
    - exact pb_prod_is_inverse.
End PullbackProduct.