Library UniMath.CategoryTheory.ModelCategories.Retract

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.opp_precat.

Declare Scope retract.
Delimit Scope morcls with retract.

Local Open Scope retract.

Local Open Scope cat.

Definition is_retract {C : category} {a b a' b' : C} (f : a --> b) (f' : a' --> b')
    (ia : a' --> a) (ra : a --> a') (ib : b' --> b) (rb : b --> b') : UU :=
  (ra ∘ ia = identity a') × (rb ∘ ib = identity b') × (f ∘ ia = ib ∘ f') × (f' ∘ ra = rb ∘ f).

Definition make_is_retract {C : category} {a b a' b' : C} {f : a --> b} {f' : a' --> b'}
    {ia : a' --> a} {ra : a --> a'} {ib : b' --> b} {rb : b --> b'}
    (ha : ra ∘ ia = identity a') (hb : rb ∘ ib = identity b') (hi : f ∘ ia = ib ∘ f') (hr : f' ∘ ra = rb ∘ f): is_retract f f' ia ra ib rb :=
  make_dirprod ha (make_dirprod hb (make_dirprod hi hr)).

Definition retract {C : category} {a b a' b' : C} (f : a --> b) (f' : a' --> b') : UU :=
  ∑ (ia : a' --> a) (ra : a --> a') (ib : b' --> b) (rb : b --> b'), is_retract f f' ia ra ib rb.

Definition make_retract {C : category} {a b a' b' : C} {f : a --> b} {f' : a' --> b'}
    (ia : a' --> a) (ra : a --> a') (ib : b' --> b) (rb : b --> b') (r : is_retract f f' ia ra ib rb) : retract f f' :=
  tpair _ ia (tpair _ ra (tpair _ ib (tpair _ rb r))).

Lemma retract_is_iso {C : category} {a b a' b' : C} {f : iso a b} {f' : a' --> b'} (r : retract f f') : is_iso f'.
Proof.
  destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].

  apply is_iso_from_is_z_iso.

  exists (ra ∘ (inv_from_iso f) ∘ ib).
  split.
  - rewrite assoc, <- hi, assoc.
    rewrite <- (assoc ia _ _).
    rewrite iso_inv_after_iso, id_right.
    exact ha.
  - rewrite <- assoc, <- assoc, hr, assoc, assoc.
    rewrite <- (assoc ib _ _).
    rewrite iso_after_iso_inv, id_right.
    exact hb.
Defined.

Lemma functor_on_retract {C D : category} (F : functor C D) {a b a' b' : C} {f : a --> b} {f' : a' --> b'} (r : retract f f') :
  retract (#F f) (#F f').
Proof.
  destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].
  use (make_retract (#F ia) (#F ra) (#F ib) (#F rb)).
  use make_is_retract; repeat rewrite <- functor_comp; try rewrite <- functor_id.
  - now rewrite ha.
  - now rewrite hb.
  - now rewrite hi.
  - now rewrite hr.
Defined.

Definition opp_retract {C : category} {a b a' b' : C} {f : a --> b} {f' : a' --> b'} (r : retract f f') :
    retract (C:=op_cat C) (opp_mor f) (opp_mor f').
Proof.
  destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]].
  use make_retract.
  - exact (opp_mor rb).
  - exact (opp_mor ib).
  - exact (opp_mor ra).
  - exact (opp_mor ia).
  - use make_is_retract.
    * exact hb.
    * exact ha.
    * symmetry. exact hr.
    * symmetry. exact hi.
Defined.

Definition retract_self {C : category} {a b : C} (f : a --> b) :
    retract f f.
Proof.
  use make_retract; try exact (identity _).
  use make_is_retract; rewrite id_left; try rewrite id_right; trivial.
Defined.