/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Module: init.equiv
Author: Jeremy Avigad, Jakob von Raumer

Ported from Coq HoTT
-/

prelude
import .path .function
open eq function

/- Equivalences -/

-- This is our definition of equivalence. In the HoTT-book it's called
-- ihae (half-adjoint equivalence).
structure is_equiv [class] {A B : Type} (f : A → B) :=
  (inv : B → A)
  (retr : (f ∘ inv) ∼ id)
  (sect : (inv ∘ f) ∼ id)
  (adj : Πx, retr (f x) = ap f (sect x))


-- A more bundled version of equivalence
structure equiv (A B : Type) :=
  (to_fun : A → B)
  (to_is_equiv : is_equiv to_fun)


namespace is_equiv
  /- Some instances and closure properties of equivalences -/
  postfix `⁻¹` := inv

  section
  variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}

  -- The identity function is an equivalence.
  definition is_equiv_id : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)

  -- The composition of two equivalences is, again, an equivalence.
  definition is_equiv_compose [Hf : is_equiv f] [Hg : is_equiv g] : (is_equiv (g ∘ f)) :=
    is_equiv.mk ((inv f) ∘ (inv g))
               (λc, ap g (retr f (g⁻¹ c)) ⬝ retr g c)
               (λa, ap (inv f) (sect g (f a)) ⬝ sect f a)
               (λa, (whisker_left _ (adj g (f a))) ⬝
                    (ap_con g _ _)⁻¹ ⬝
                    ap02 g (ap_con_eq_con (retr f) (sect g (f a))⁻¹ ⬝
                            (ap_compose (inv f) f _ ◾  adj f a) ⬝
                            (ap_con f _ _)⁻¹
                           ) ⬝
                    (ap_compose f g _)⁻¹
               )

  -- Any function equal to an equivalence is an equivlance as well.
  definition is_equiv_eq_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') :=
     eq.rec_on Heq Hf

  -- Any function pointwise equal to an equivalence is an equivalence as well.
  definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') :=
    let sect' := (λ b, (Hty (inv f b))⁻¹ ⬝ retr f b) in
    let retr' := (λ a, (ap (inv f) (Hty a))⁻¹ ⬝ sect f a) in
    let adj' := (λ (a : A),
      let ff'a := Hty a in
      let invf := inv f in
      let secta := sect f a in
      let retrfa := retr f (f a) in
      let retrf'a := retr f (f' a) in
      have eq1 : _ = _,
        from calc ap f secta ⬝ ff'a
              = retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _)
          ... = ap (f ∘ invf) ff'a ⬝ retrf'a : ap_con_eq_con
          ... = ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f,
      have eq2 : _ = _,
        from calc retrf'a
              = (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : eq_inv_con_of_con_eq _ _ _ (eq1⁻¹)
          ... = ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_inv invf ff'a
          ... = ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : ap_con_eq_con_ap
          ... = (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : con.assoc
          ... = (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_inv
          ... = (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_con_eq_con_ap
          ... = (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_inv
          ... = Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : con.assoc,
      have eq3 : _ = _,
        from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a
              = (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : inv_con_eq_of_eq_con _ _ _ eq2
          ... = (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_inv
          ... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_con,
    eq3) in
  is_equiv.mk (inv f) sect' retr' adj'
  end

  context
  parameters {A B : Type} (f : A → B) (g : B → A)
            (ret : f ∘ g ∼ id) (sec : g ∘ f ∼ id)

  private definition adjointify_sect' : g ∘ f ∼ id :=
    (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x)

  private definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) :=
    (λ (a : A),
      let fgretrfa := ap f (ap g (ret (f a))) in
      let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in
      let fgfa := f (g (f a)) in
      let retrfa := ret (f a) in
      have eq1 : ap f (sec a) = _,
        from calc ap f (sec a)
              = idp ⬝ ap f (sec a) : !idp_con⁻¹
          ... = (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : {!con.left_inv⁻¹}
          ... = ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!con_ap_eq_con⁻¹}
          ... = ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
          ... = (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !con.assoc,
      have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)),
        from !con_idp ⬝ eq1,
      have eq3 : idp = _,
        from calc idp
              = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : eq_inv_con_of_con_eq _ _ _ eq2
          ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !con.assoc'
          ... = (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_inv⁻¹}
          ... = ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !con.assoc'
          ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!con_ap_eq_con⁻¹}
          ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
          ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!con.assoc'⁻¹}
          ... = retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_con⁻¹}
          ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !con.assoc'⁻¹
          ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_con⁻¹},
      have eq4 : ret (f a) = ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a),
        from eq_of_idp_eq_inv_con _ _ eq3,
      eq4)

  definition adjointify : is_equiv f :=
    is_equiv.mk g ret adjointify_sect' adjointify_adj'

  end

  section
  variables {A B: Type} (f : A → B)

  --The inverse of an equivalence is, again, an equivalence.
  definition is_equiv_inv [instance] [Hf : is_equiv f] : (is_equiv (inv f)) :=
    adjointify (inv f) f (sect f) (retr f)
  end

  section
  variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f]
  include Hf

  variable (g : B → C)

  definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
    have Hfinv [visible] : is_equiv (f⁻¹), from is_equiv_inv f,
    @homotopy_closed _ _ _ _ (is_equiv_compose (f⁻¹) (g ∘ f)) (λb, ap g (@retr _ _ f _ b))

  definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
    have Hfinv [visible] : is_equiv (f⁻¹), from is_equiv_inv f,
    @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) (f⁻¹)) (λa, sect f (g a))

  --Rewrite rules
  definition eq_of_eq_inv {x : A} {y : B} (p : x = (inv f) y) : (f x = y) :=
    (ap f p) ⬝ (@retr _ _ f _ y)

  definition eq_of_inv_eq {x : A} {y : B} (p : (inv f) y = x) : (y = f x) :=
    (eq_of_eq_inv f (p⁻¹))⁻¹

  definition inv_eq_of_eq {x : B} {y : A} (p : x = f y) : (inv f) x = y :=
    ap (f⁻¹) p ⬝ sect f y

  definition eq_inv_of_eq {x : B} {y : A} (p : f y = x) : y = (inv f) x :=
    (inv_eq_of_eq f (p⁻¹))⁻¹

  definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) :=
    adjointify (ap f)
      (λq, (inverse (sect f x)) ⬝ ap (f⁻¹) q ⬝ sect f y)
      (λq, !ap_con
        ⬝ whisker_right !ap_con _
        ⬝ ((!ap_inv ⬝ inverse2 ((adj f _)⁻¹))
          ◾ (inverse (ap_compose (f⁻¹) f _))
          ◾ (adj f _)⁻¹)
        ⬝ con_ap_con_eq_con_con (retr f) _ _
        ⬝ whisker_right !con.right_inv _
        ⬝ !idp_con)
      (λp, whisker_right (whisker_left _ ((ap_compose f (f⁻¹) _)⁻¹)) _
        ⬝ con_ap_con_eq_con_con (sect f) _ _
        ⬝ whisker_right !con.right_inv _
        ⬝ !idp_con)

  -- The function equiv_rect says that given an equivalence f : A → B,
  -- and a hypothesis from B, one may always assume that the hypothesis
  -- is in the image of e.

  -- In fibrational terms, if we have a fibration over B which has a section
  -- once pulled back along an equivalence f : A → B, then it has a section
  -- over all of B.

  definition equiv_rect (P : B → Type) :
      (Πx, P (f x)) → (Πy, P y) :=
    (λg y, eq.transport _ (retr f y) (g (f⁻¹ y)))

  definition equiv_rect_comp (P : B → Type)
      (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
    calc equiv_rect f P df (f x)
          = transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp
      ... = transport P (eq.ap f (sect f x)) (df (f⁻¹ (f x))) : adj f
      ... = transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose
      ... = df x : apD df (sect f x)

  end

  --Transporting is an equivalence
  definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
    is_equiv.mk (transport P (p⁻¹)) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p)


end is_equiv

open is_equiv
namespace equiv

  attribute to_is_equiv [instance]

  infix `≃`:25 := equiv

  context
  parameters {A B C : Type} (eqf : A ≃ B)

  private definition f : A → B := to_fun eqf
  private definition Hf [instance] : is_equiv f := to_is_equiv eqf

  protected definition refl : A ≃ A := equiv.mk id is_equiv.is_equiv_id

  definition trans (eqg: B ≃ C) : A ≃ C :=
    equiv.mk ((to_fun eqg) ∘ f)
             (is_equiv_compose f (to_fun eqg))

  definition equiv_of_eq_of_equiv (f' : A → B) (Heq : to_fun eqf = f') : A ≃ B :=
    equiv.mk f' (is_equiv.is_equiv_eq_closed f Heq)

  definition symm : B ≃ A :=
    equiv.mk (is_equiv.inv f) !is_equiv.is_equiv_inv

  definition equiv_ap (P : A → Type) {x y : A} {p : x = y} : (P x) ≃ (P y) :=
    equiv.mk (eq.transport P p) (is_equiv_tr P p)

  end

  --we need this theorem for the funext_of_ua proof
  theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
    eq.rec_on p idp

  -- calc enviroment
  -- Note: Calculating with substitutions needs univalence
  calc_trans equiv.trans
  calc_refl equiv.refl
  calc_symm equiv.symm

end equiv