Library UniMath.CategoryTheory.limits.pullbacks_slice_products_equiv

**********************************************************

Matthew Weaver, 2017

**********************************************************

Contents : Equivalence of binary products in C/Z to pullbacks of pairs of arrows to Z in C

Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.slicecat.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.pullbacks.

Local Open Scope cat.

Proof that the types of binary products in C/Z and pullbacks of pairs of arrows to Z in C are equivalent

Section pullbacks_slice_products_equiv.

  Definition some_pullback (C : precategory) (Z : C) : UU :=
    ∑ A B (f : A --> Z) (g : B --> Z) , Pullback f g.

  Definition some_binprod (C : precategory) : UU :=
    ∑ A B , BinProduct C A B.

  Context {C : precategory} (hsC : has_homsets C).
  Local Notation "C / X" := (slice_precat C X hsC).

  Lemma isPullback_to_isBinProduct {Z : C} {AZ BZ PZ : C / Z} {l : PZ --> AZ} {r : PZ --> BZ} :
     isPullback (pr2 AZ) (pr2 BZ) (pr1 l) (pr1 r) (! (pr2 l) @ (pr2 r)) → isBinProduct (C / Z) AZ BZ PZ l r.
  Show proof.

    induction AZ as [A f].
    induction BZ as [B g].
    induction PZ as [P h].
    induction l as [l leq].
    induction r as [r req].
    intros isPull [Y i] [j jeq] [k keq]; simpl in *.
    unfold isPullback in isPull. specialize isPull with Y j k.
    use unique_exists.
    + use tpair.
      ++ apply isPull.
         abstract (simpl; now rewrite <- jeq , keq).
      ++ abstract (simpl; now rewrite leq, assoc, (pr1 (pr2 (pr1 (isPull _)))), jeq).
    + abstract (split; apply (eq_mor_slicecat hsC); simpl;
                [apply (pr1 (pr2 (pr1 (isPull _)))) | apply (pr2 (pr2 (pr1 (isPull _))))]).
    + abstract (now intros q; apply isapropdirprod; apply (has_homsets_slice_precat hsC)).
    + abstract (intros q [H1 H2]; apply (eq_mor_slicecat hsC);
                use (maponpaths pr1 ((pr2 (isPull _)) ((pr1 q) ,, (_ ,, _))));
                [apply (maponpaths pr1 H1) | apply (maponpaths pr1 H2)]).

  Lemma slice_isBinProduct_to_isPullback
        {A B Z P : C} {f : A --> Z} {g : B --> Z} {l : P --> A} {r : P --> B} {e : l · f = r · g} :
    isBinProduct (C / Z) (A ,, f) (B ,, g) (P ,, l · f) (l ,, idpath _) (r ,, e) → isPullback f g l r e.
  Show proof.

    intros PisProd Y j k Yeq.
    use unique_exists.
    + exact (pr1 (pr1 (pr1 (PisProd (Y ,, j · f) (j ,, idpath _) (k ,, Yeq))))).
    + abstract (exact (maponpaths pr1 (pr1 (pr2 (pr1 (PisProd (Y ,, j · f) (j ,, idpath _) (k ,, Yeq))))) ,,
                                  maponpaths pr1 (pr2 (pr2 (pr1 (PisProd (Y ,, j · f) (j ,, idpath _) (k ,, Yeq))))))).
    + abstract (intros x; apply isofhleveldirprod; apply (hsC _ _)).
    + intros t teqs.
      use (maponpaths pr1 (maponpaths pr1 (pr2 (PisProd (Y ,, j · f) (j ,, idpath _) (k ,, Yeq))
                                                  ((t ,, (maponpaths (λ x, x · f) (!(pr1 teqs)) @ !(assoc _ _ _) @ maponpaths (λ x, t · x) (idpath _))) ,, _)))).
      abstract (split; apply eq_mor_slicecat; [exact (pr1 teqs) | exact (pr2 teqs)]).

equivalence of function taking proof of isPullback to proof of isBinProduct

  Lemma isweq_isPullback_to_isBinProduct {Z : C} {AZ BZ PZ : C / Z} {l : PZ --> AZ} {r : PZ --> BZ} :
    isweq (@isPullback_to_isBinProduct Z AZ BZ PZ l r).
  Show proof.

    apply isweqimplimpl.
    + induction AZ as [A f].
      induction BZ as [B g].
      induction PZ as [P h].
      induction l as [l leq].
      induction r as [r req].
      simpl in *. induction (! leq).
      assert (H : leq = idpath (l · f)) by apply hsC.
      intros PisProd.
      apply slice_isBinProduct_to_isPullback; simpl.
      rewrite <- H.
      exact PisProd.
    + apply isaprop_isPullback.
    + apply isaprop_isBinProduct.

equivalence of function taking proof of isBinProduct to proof of isPullback

  Lemma isweq_slice_isBinProduct_to_isPullback
        {A B Z P : C} {f : A --> Z} {g : B --> Z} {l : P --> A} {r : P --> B} {e : l · f = r · g} :
    isweq (@slice_isBinProduct_to_isPullback A B Z P f g l r e).
  Show proof.

    apply isweqimplimpl.
    + intros isPull.
      now apply isPullback_to_isBinProduct.
    + now apply isaprop_isBinProduct.
    + now apply isaprop_isPullback.

Context (Z : C).

pullback_to_slice_binprod is invertible

  Lemma pullback_to_slice_binprod_inv {A B : C} {f : A --> Z} {g : B --> Z} (P : Pullback f g) :
    slice_binprod_to_pullback hsC (pullback_to_slice_binprod hsC P) = P.
  Show proof.

    induction P as [[P [l r]] [Peq PisPull]].
    apply (invmaponpathsincl pr1).
    { apply isinclpr1.
      intros ?.
      apply isofhleveltotal2.
      + apply hsC.
      + intros ?.
        apply isaprop_isPullback.
    }
    reflexivity.

slice_binprod_to_pullback is invertible

  Lemma slice_binprod_to_pullback_inv {AZ BZ : C / Z} (P : BinProduct (C / Z) AZ BZ) :
    pullback_to_slice_binprod hsC (slice_binprod_to_pullback hsC P) = P.
  Show proof.

    induction AZ as [A f].
    induction BZ as [B g].
    induction P as [[[P h] [[l leq] [r req]]] PisProd].
    apply (invmaponpathsincl pr1).
    { apply isinclpr1.
      intros ?.
      apply isaprop_isBinProduct.
    }
    simpl in *.
    use total2_paths2_f.
    + apply (total2_paths2_f (idpath _)).
      rewrite idpath_transportf.
      exact (!leq).
    + induction (!leq). simpl.
      rewrite idpath_transportf.
      use total2_paths2_f.
    - now apply (eq_mor_slicecat hsC).
    - rewrite transportf_const.
      now apply (eq_mor_slicecat hsC).

function taking the type of all binary products in C / Z

to the type of all pullbacks of functions to Z in C

Definition binprod_to_pullback : some_binprod (C / Z) → some_pullback C Z.
Show proof.

    intro P.
    induction P as [AZ BZ].
    induction BZ as [BZ P].
    exact (pr1 AZ ,, pr1 BZ ,, pr2 AZ ,, pr2 BZ ,, slice_binprod_to_pullback hsC P).

function taking the type of all pullbacks of functions to Z in C

to the type of all binary products in C / Z

Definition pullback_to_binprod : some_pullback C Z → some_binprod (C / Z).
Show proof.

intros [A [B [f [g P]]]].
use ((A ,, f) ,, (B ,, g) ,, pullback_to_slice_binprod hsC P).

binprod_to_pullback is invertible

  Lemma binprod_to_pullback_inv (P : some_binprod (C / Z)) :
    pullback_to_binprod (binprod_to_pullback P) = P.
  Show proof.

    induction P as [[A f] [[B g] P]].
    unfold pullback_to_binprod , binprod_to_pullback.
    simpl.
    repeat (apply (total2_paths2_f (idpath _)); rewrite idpath_transportf).
    exact (slice_binprod_to_pullback_inv P).

pullback_to_binprod is invertible

  Lemma pullback_to_binprod_inv (P : some_pullback C Z) :
    binprod_to_pullback (pullback_to_binprod P) = P.
  Show proof.

    induction P as [A [B [f [g P]]]].
    unfold binprod_to_pullback , pullback_to_binprod.
    do 4 (apply (total2_paths2_f (idpath _)); rewrite idpath_transportf).
    exact (pullback_to_slice_binprod_inv P).

Definition isweq_binprod_to_pullback : isweq binprod_to_pullback :=
isweq_iso _ _ binprod_to_pullback_inv pullback_to_binprod_inv.

the equivalence of the types of binary products in C/Z

and pullbacks of pairs of arrows to Z in C

Definition weq_binprod_to_pullback : weq (some_binprod (C / Z)) (some_pullback C Z) :=
binprod_to_pullback ,, isweq_binprod_to_pullback.

End pullbacks_slice_products_equiv.