rel_contr.hlean

import function

open eq function is_equiv equiv is_trunc unit trunc

structure is_rel_contr (X Y : Type) :=
  (to_fun : X → Y)
  (surj   : is_split_surjective to_fun)

definition is_rel_contr_reflexive (X : Type) : is_rel_contr X X :=
is_rel_contr.mk id (λ y, fiber.mk y idp)

definition is_rel_contr_transitive (X Y Z : Type) (c : is_rel_contr X Y)
  (d : is_rel_contr Y Z) : is_rel_contr X Z :=
begin
  induction c with [fc, pc], induction d with [fd, pd],
  fapply is_rel_contr.mk, exact fd ∘ fc,
  intro z, induction (pd z) with [y, yeq], induction (pc y) with [x, xeq],
  fapply fiber.mk, exact x, esimp[compose], rewrite [xeq, yeq],
end

definition is_rel_contr_contr (X Y : Type) [cc : is_contr Y] (x : X) : is_rel_contr X Y :=
is_rel_contr.mk (λ x, center Y) (λ y, fiber.mk x !center_eq)

definition is_rel_contr_sigma (X Y : Type) (P : Y → Type) (cX : is_rel_contr X Y)
  (cY : Π y, is_rel_contr X (P y)) :
  is_rel_contr X (sigma P) :=
begin
  induction cX with [fX, Hfx], fapply is_rel_contr.mk,
  { intro x, fapply sigma.mk, exact fX x,
    induction cY (fX x) with [fY, Hfy], exact fY x },
  { esimp[is_split_surjective] at *, intro b, induction b with [y, py],
    induction Hfx y with [pp, ppeq], apply fiber.mk pp, apply sigma.sigma_eq ppeq,
    esimp, induction cY (fX pp) with [f, s], esimp, induction ppeq, esimp,
    apply pathover_of_tr_eq, esimp[is_split_surjective] at *, esimp,
  },
end

definition is_contr_equiv_is_rel_contr (X : Type) :
  is_contr X ≃ is_rel_contr unit X :=
begin
  fapply equiv.MK,
  { intro cc, fapply is_rel_contr.mk, intro x, exact center X, 
    intro y, exact fiber.mk  ⋆ !center_eq, },
  { intro rc, induction rc with [f, ss], apply is_contr.mk (f ⋆),
    intro x, induction (ss x) with [pp, Hpp], induction pp, exact Hpp, },
  { intro rc, induction rc with [f, ss], fapply apd011 is_rel_contr.mk,
    apply eq_of_homotopy, intro u, induction u,
    assert H : is_contr X, apply is_contr.mk (f ⋆),
      intro x, induction (ss x) with [pp, Hpp], induction pp, exact Hpp,
    apply eq_of_is_contr,
    esimp, apply eq_of_homotopy, intro b, induction (ss b) with [u, Hu],
    induction u, esimp,
  },
  { intro cc, apply is_hprop.elim, },
end

structure is_rel_contr' (X Y : Type) :=
  (to_fun : X → Y)
  (surj   : is_surjective to_fun)

definition is_rel_contr'_reflexive (X : Type) : is_rel_contr' X X :=
begin
  fapply is_rel_contr'.mk, apply id,
  esimp[is_surjective], intro x, apply tr, exact fiber.mk x idp,
end

definition is_rel_contr'_unit (X : Type) :
  is_contr X ≃ is_rel_contr' unit X :=
begin
  fapply equiv.MK,
  { intro cc, fapply is_rel_contr'.mk, intro u, exact center X, 
    intro x, apply tr, exact fiber.mk ⋆ !center_eq },
  { intro rc, induction rc with [f, Hf], fapply is_contr.mk, exact f ⋆,
    intro x, esimp[is_surjective] at Hf, induction (Hf x), 
    /-induction a, induction point,  exact point_eq -/},
  { intro rc, induction rc with [f, Hf], fapply apd011 is_rel_contr'.mk, 
    apply eq_of_homotopy, intro u, induction u,
    assert H : is_contr X, fapply is_contr.mk, exact f ⋆,
      intro x, esimp[is_surjective] at Hf, induction (Hf x), 
      induction a, induction point,  exact point_eq, 
    apply eq_of_is_contr, apply is_hprop.elim, },
  { intro cc, apply is_hprop.elim, },
end 


print definition is_surjective
check eq_of_is_contr
check @trunc.elim
check @equiv.MK
check apd011
check ap011