Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

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.Core.Functors.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.equalizers.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Monics.

Local Open Scope cat.

Section def_pb.

  Context (C : category).

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

Lemma isaprop_isPullback {a b c d : C} (f : b --> a) (g : c --> a)
        (p1 : d --> b) (p2 : d --> c) (H : p1 · f = p2 · g) :
       isaprop (isPullback f g p1 p2 H).
Show proof.

Lemma PullbackArrowUnique {a b c d : C} (f : b --> a) (g : c --> a)
        (p1 : d --> b) (p2 : d --> c) (H : p1 · f = p2 · g)
     (P : isPullback f g p1 p2 H) e (h : e --> b) (k : e --> c)
     (Hcomm : h · f = k · g)
     (w : e --> d)
     (H1 : w · p1 = h) (H2 : w · p2 = k) :
     w = (pr1 (pr1 (P e h k Hcomm))).
Show proof.

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

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

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

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

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

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

Definition PullbackSqrCommutes {a b c : C} {f : b --> a} {g : c --> a}
   (Pb : Pullback f g) :
    PullbackPr1 Pb · f = PullbackPr2 Pb · g .
Show proof.

Definition isPullback_Pullback {a b c : C} {f : b --> a} {g : c --> a}
   (P : Pullback f g) :
  isPullback f g (PullbackPr1 P) (PullbackPr2 P) (PullbackSqrCommutes P).
Show proof.

Definition PullbackArrow {a b c : C} {f : b --> a} {g : c --> a}
   (Pb : Pullback f g) e (h : e --> b) (k : e --> c) (H : h · f = k · g) : e --> Pb :=
   pr1 (pr1 (isPullback_Pullback Pb e h k H)).

Lemma PullbackArrowUnique' {a b c : C} (f : C⟦b,a⟧) (g : C⟦c,a⟧)
      (P : Pullback f g) e (h : C⟦e,b⟧) (k : C⟦e,c⟧)
      (Hcomm : h · f = k · g) (w : C⟦e,P⟧) (H1 : w · PullbackPr1 P = h) (H2 : w · PullbackPr2 P = k) :
  w = PullbackArrow P e h k Hcomm.
Show proof.

Lemma PullbackArrow_PullbackPr1 {a b c : C} {f : b --> a} {g : c --> a}
   (Pb : Pullback f g) e (h : e --> b) (k : e --> c) (H : h · f = k · g) :
   PullbackArrow Pb e h k H · PullbackPr1 Pb = h.
Show proof.

Lemma PullbackArrow_PullbackPr2 {a b c : C} {f : b --> a} {g : c --> a}
   (Pb : Pullback f g) e (h : e --> b) (k : e --> c) (H : h · f = k · g) :
   PullbackArrow Pb e h k H · PullbackPr2 Pb = k.
Show proof.

Definition make_Pullback {a b c : C} (f : C⟦b, a⟧) (g : C⟦c, a⟧)
    (d : C) (p1 : C⟦d,b⟧) (p2 : C ⟦d,c⟧)
    (H : p1 · f = p2 · g)
    (ispb : isPullback f g p1 p2 H)
  : Pullback f g.
Show proof.

Definition make_isPullback {a b c d : C} (f : C ⟦b, a⟧) (g : C ⟦c, a⟧)
           (p1 : C⟦d,b⟧) (p2 : C⟦d,c⟧) (H : p1 · f = p2 · g) :
  (∏ e (h : C ⟦e, b⟧) (k : C⟦e,c⟧) (Hk : h · f = k · g ),
   ∃! hk : C⟦e,d⟧, (hk · p1 = h) × (hk · p2 = k)) →
  isPullback f g p1 p2 H.
Show proof.

Local Lemma postCompWithPullbackArrow_subproof
 {c d a b x : C} (k0 : C⟦c,d⟧) {f : C⟦a,x⟧} {g : C⟦b,x⟧}
 {h : C ⟦ d, a ⟧} {k : C ⟦ d, b ⟧} (H : h · f = k · g) :
  k0 · h · f = k0 · k · g.
Show proof.

Lemma postCompWithPullbackArrow
 (c d : C) (k0 : C⟦c,d⟧) {a b x : C} {f : C⟦a,x⟧} {g : C⟦b,x⟧}
 (Pb : Pullback f g)
 (h : C ⟦ d, a ⟧) (k : C ⟦ d, b ⟧) (H : h · f = k · g) :
   k0 · PullbackArrow Pb d h k H =
   PullbackArrow Pb _ (k0 · h) (k0 · k) (postCompWithPullbackArrow_subproof k0 H).
Show proof.

Lemma MorphismsIntoPullbackEqual {a b c d : C} {f : b --> a} {g : c --> a}
        {p1 : d --> b} {p2 : d --> c} {H : p1 · f = p2 · g}
        (P : isPullback f g p1 p2 H) {e}
        (w w': e --> d)
        (H1 : w · p1 = w' · p1) (H2 : w · p2 = w' · p2)
     : w = w'.
Show proof.

Definition identity_is_Pullback_input {a b c : C} {f : b --> a} {g : c --> a} (Pb : Pullback f g) :
  ∑ hk : Pb --> Pb,
   (hk · PullbackPr1 Pb = PullbackPr1 Pb) × (hk · PullbackPr2 Pb = PullbackPr2 Pb).
Show proof.

Lemma PullbackEndo_is_identity {a b c : C} {f : b --> a} {g : c --> a}
   (Pb : Pullback f g) (k : Pb --> Pb) (kH1 : k · PullbackPr1 Pb = PullbackPr1 Pb)
                                       (kH2 : k · PullbackPr2 Pb = PullbackPr2 Pb) :
       identity Pb = k.
Show proof.

Definition from_Pullback_to_Pullback {a b c : C} {f : b --> a} {g : c --> a}
   (Pb Pb': Pullback f g) : Pb --> Pb'.
Show proof.

Lemma are_inverses_from_Pullback_to_Pullback {a b c : C} {f : b --> a} {g : c --> a}
   (Pb Pb': Pullback f g) :
is_inverse_in_precat (from_Pullback_to_Pullback Pb Pb')
  (from_Pullback_to_Pullback Pb' Pb).
Show proof.

Lemma isziso_from_Pullback_to_Pullback {a b c : C} {f : b --> a} {g : c --> a}
   (Pb Pb': Pullback f g) :
      is_z_isomorphism (from_Pullback_to_Pullback Pb Pb').
Show proof.

Definition z_iso_from_Pullback_to_Pullback {a b c : C}{f : b --> a} {g : c --> a}
   (Pb Pb': Pullback f g) : z_iso Pb Pb' :=
  _ ,, isziso_from_Pullback_to_Pullback Pb Pb'.

Lemma pullbackiso {A B D:C} {f : A --> D} {g : B --> D}
      (pb : Pullback f g) (pb' : Pullback f g)
  : ∑ (t : z_iso (PullbackObject pb) (PullbackObject pb')),
    t · PullbackPr1 pb' = PullbackPr1 pb ×
    t · PullbackPr2 pb' = PullbackPr2 pb.
Show proof.

Section pullback_lemma.

Context (a b c d e x : C)
  (f : b --> a) (g : c --> a) (h : e --> b) (k : e --> c)
  (i : d --> b) (j : x --> e) (m : x --> d)
  (H1 : h · f = k · g) (H2 : m · i = j · h)
  (P1 : isPullback _ _ _ _ H1) (P2 : isPullback _ _ _ _ H2).

Lemma glueSquares : m · (i · f) = (j · k) · g.
Show proof.

Lemma isPullbackGluedSquare : isPullback (i · f) g m (j · k) glueSquares.
Show proof.

End pullback_lemma.

Definition pullback_glue_pullback {a b c e : C} {f : b --> a} {g : c --> a} {h : e --> b} (pbr : Pullback f g) (pbl : Pullback h (PullbackPr1 pbr)) : Pullback (h · f) g.
Show proof.

End def_pb.

Arguments isPullback [_ _ _ _ _ _ _ _ _] _.
Arguments Pullback [_ _ _ _] _ _.
Arguments PullbackArrow [_ _ _ _ _ _ ] _ _ _ _ _ .
Arguments make_Pullback [_ _ _ _ _ _ _ _ _] _ _.
Arguments PullbackObject [_ _ _ _ _ _ ] _.
Arguments z_iso_from_Pullback_to_Pullback [_ _ _ _ _ _] _ _.
Arguments from_Pullback_to_Pullback [_ _ _ _ _ _] _ _.
Arguments are_inverses_from_Pullback_to_Pullback [_ _ _ _ _ _] _ _.
Arguments PullbackPr1 [_ _ _ _ _ _] _.
Arguments PullbackPr2 [_ _ _ _ _ _] _.
Arguments isPullback_Pullback [_ _ _ _ _ _] _.
Arguments MorphismsIntoPullbackEqual [_ _ _ _ _ _ _ _ _ _] _ _ _ _ .
Arguments PullbackSqrCommutes [_ _ _ _ _ _] _.
Arguments PullbackArrow_PullbackPr1 [_ _ _ _ _ _] _ _ _ _ _.
Arguments PullbackArrow_PullbackPr2 [_ _ _ _ _ _] _ _ _ _ _.
Arguments PullbackArrowUnique [_ _ _ _ _ _ _ _ _ ] _ _ _ _ _ _ _ _ _ .

Section Universal_Unique.

  Context (C : category) (H : is_univalent C).

Lemma inv_from_z_iso_z_iso_from_Pullback (a b c : C) (f : b --> a) (g : c --> a)
  (Pb : Pullback f g) (Pb' : Pullback f g):
    inv_from_z_iso (z_iso_from_Pullback_to_Pullback Pb Pb') = from_Pullback_to_Pullback Pb' Pb.
Show proof.

Lemma isaprop_Pullbacks: isaprop (Pullbacks C).
Show proof.

End Universal_Unique.

Arguments Pullbacks : clear implicits.

Section monic_pb.

  Context (C : category).

  Lemma MonicPullbackisMonic {a b c : C} (M : Monic _ b a) (g : c --> a)
        (PB : Pullback M g) : isMonic (PullbackPr2 PB).
  Show proof.

  Lemma MonicPullbackisMonic' {a b c : C} (f : b --> a) (M : Monic _ c a)
        (PB : Pullback f M) : isMonic (PullbackPr1 PB).
  Show proof.

End monic_pb.

Arguments glueSquares {_ _ _ _ _ _ _ _ _ _ _ _ _ _ } _ _ .
Arguments isPullbackGluedSquare [_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _] _ _ [_ _ _] _.

Section pb_criteria.

  Context (C : category).

  Lemma Pullback_from_Equalizer_BinProduct_eq (X Y Z : C)
             (f : X --> Z) (g : Y --> Z) (BinProd : BinProduct C X Y)
             (Eq : Equalizer ((BinProductPr1 C BinProd) · f)
                             ((BinProductPr2 C BinProd) · g)) :
    EqualizerArrow Eq · (BinProductPr1 C BinProd) · f
    = EqualizerArrow Eq · (BinProductPr2 C BinProd) · g.
  Show proof.

  Definition Pullback_from_Equalizer_BinProduct_isPullback (X Y Z : C)
             (f : X --> Z) (g : Y --> Z) (BinProd : BinProduct C X Y)
             (Eq : Equalizer ((BinProductPr1 C BinProd) · f)
                             ((BinProductPr2 C BinProd) · g)) :
    isPullback
               (Pullback_from_Equalizer_BinProduct_eq
                  X Y Z f g BinProd Eq).
  Show proof.

  Definition Pullback_from_Equalizer_BinProduct (X Y Z : C)
             (f : X --> Z) (g : Y --> Z) (BinProd : BinProduct C X Y)
             (Eq : Equalizer ((BinProductPr1 C BinProd) · f)
                             ((BinProductPr2 C BinProd) · g)) :
    Pullback f g.
  Show proof.

  Definition Pullbacks_from_Equalizers_BinProducts (BinProds : BinProducts C)
             (Eqs : Equalizers C) : Pullbacks C.
  Show proof.

End pb_criteria.

Section lemmas_on_pullbacks.

                k
          d --------> c
          |           |
       h  |     H     | g
          v           v
          b --------> a
               f

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

Lemma is_symmetric_isPullback
  : isPullback H -> isPullback (!H).
Show proof.

Definition pb_of_section (isPb : isPullback H)
  (s : C⟦a,c⟧) (K : s · g = identity _ )
  : ∑ s' : C⟦b, d⟧, s' · h = identity _ .
Show proof.

Definition section_from_diagonal (isPb : isPullback H)
  : (∑ x : C⟦b, c⟧, x · g = f)
    ->
    ∑ s' : C⟦b, d⟧, s' · h = identity _ .
Show proof.

Definition diagonal_from_section (isPb : isPullback H)
  : (∑ x : C⟦b, c⟧, x · g = f)
    <-
    ∑ s' : C⟦b, d⟧, s' · h = identity _ .
Show proof.

Definition weq_section_from_diagonal (isPb : isPullback H)
  : (∑ x : C⟦b, c⟧, x · g = f)
    ≃
    ∑ s' : C⟦b, d⟧, s' · h = identity _ .
Show proof.

              i'           k
         d' -------> d --------> c
         |           |           |
       h'|           |h          | g
         v           v           v
         b'--------> b --------> a
              i            f

Lemma isPullback_two_pullback
     (b' d' : C) (h' : C⟦d', b'⟧)
     (i : C⟦b', b⟧) (i' : C⟦d', d⟧)
     (Hinner : h · f = k · g)
     (Hinnerpb : isPullback Hinner)
     (Hleft : h' · i = i' · h)
     (Houterpb : isPullback (glueSquares Hinner Hleft ))
     : isPullback Hleft.
Show proof.

Section pullback_iso.

              i'           k
         d' -------> d --------> c
         |           |           |
       h'|           |h          | g
         v           v           v
         b'--------> b --------> a
              i            f

Lemma isPullback_z_iso_of_morphisms (b' d' : C) (h' : C⟦d', b'⟧)
     (i : C⟦b', b⟧) (i' : C⟦d', d⟧)
     (xi : is_z_isomorphism i) (xi' : is_z_isomorphism i')
     (Hi : h' · i = i' · h)
     (H' : h' · (i · f) = (i' · k) · g)
   : isPullback H ->
     isPullback H'.
Show proof.

End pullback_iso.

End lemmas_on_pullbacks.

Definition switchPullback {C:category} {A B D:C} {f : A --> D} {g : B --> D} (pb : Pullback f g) : Pullback g f.
Show proof.

Section pb_of_ziso.

Lemma Pullback_of_z_iso {C:category} {a b c : C} {f : C ⟦b, a⟧} {g : C ⟦c, a⟧} (gis : is_z_isomorphism g) (pb : Pullback f g) : is_z_isomorphism (PullbackPr1 pb).
Show proof.

Lemma Pullback_of_z_iso' {C:category} {a b c : C} {f : C ⟦b, a⟧} {g : C ⟦c, a⟧} (fis : is_z_isomorphism f) (pb : Pullback f g) : is_z_isomorphism (PullbackPr2 pb).
Show proof.

End pb_of_ziso.

Definition Pullback_z_iso_of_morphisms {C:category} {a b c : C} {f : b --> a} {g : c --> a} (pb : Pullback f g)
  {b' pb' : C}
  (i : C⟦b', b⟧) (i' : C⟦pb', pb⟧) (h : C⟦pb', b'⟧)
  (xi : is_z_isomorphism i) (xi' : is_z_isomorphism i')
  (Hi : h · i = i' · (PullbackPr1 pb))
  : Pullback (i · f) g.
Show proof.

Section functor_on_square.

Context (C D : category) (F : functor C D).

Section isPullback_if_functor_on_square_is.

  Context (Fff : fully_faithful F)
    {a b c d : C}
    {f : C ⟦b, a⟧} {g : C ⟦c, a⟧} {h : C⟦d, b⟧} {k : C⟦d,c⟧}
    (H : h · f = k · g).

Definition functor_on_square : #F h · #F f = #F k · #F g.
Show proof.

Context (X : isPullback functor_on_square).

Lemma isPullback_preimage_square : isPullback H.
Show proof.

End isPullback_if_functor_on_square_is.

Section ff_es_functor_preserves_pb.

  Context (Fff : fully_faithful F) (Fes : essentially_surjective F).

Let FF a b := (weq_from_fully_faithful Fff a b).

Context {a b c d : C}
  {f : C ⟦b, a⟧} {g : C ⟦c, a⟧} {h : C⟦d, b⟧} {k : C⟦d,c⟧}
  (H : h · f = k · g)
  (X : isPullback H).

Lemma isPullback_image_square
  : isPullback (functor_on_square H).
Show proof.

End ff_es_functor_preserves_pb.

Definition maps_pb_square_to_pb_square
  {a b c d : C}
  {f : C ⟦b, a⟧} {g : C ⟦c, a⟧} {h : C⟦d, b⟧} {k : C⟦d,c⟧}
  (H : h · f = k · g)
  : UU :=
  isPullback H -> isPullback (functor_on_square H).

Definition maps_pb_squares_to_pb_squares :=
   ∏ (a b c d : C)
     (f : C ⟦b, a⟧) (g : C ⟦c, a⟧) (h : C⟦d, b⟧) (k : C⟦d,c⟧)
     (H : h · f = k · g),
     maps_pb_square_to_pb_square H.

End functor_on_square.