/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Floris van Doorn

Ported from Coq HoTT
Theorems about the types equiv and is_equiv
-/

import .fiber .arrow arity ..prop_trunc cubical.square .pointed

open eq is_trunc sigma sigma.ops pi fiber function equiv

namespace is_equiv
  variables {A B : Type} (f : A → B) [H : is_equiv f]
  include H
  /- is_equiv f is a mere proposition -/
  definition is_contr_fiber_of_is_equiv [instance] (b : B) : is_contr (fiber f b) :=
  is_contr.mk
    (fiber.mk (f⁻¹ b) (right_inv f b))
    (λz, fiber.rec_on z (λa p,
      fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
        right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b)
                                                           : by rewrite inv_con_cancel_left
      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)   : by rewrite ap_con_eq_con
      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite [adj f]
      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p   : by rewrite con.assoc
      ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p  : by rewrite ap_compose
      ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p    : by rewrite ap_inv
      ... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p         : by rewrite ap_con)))

  definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) :=
  begin
    fapply is_trunc_equiv_closed,
      {apply sigma_equiv_sigma_right, intro g, apply eq_equiv_homotopy},
    fapply is_trunc_equiv_closed,
      {apply fiber.sigma_char},
    fapply is_contr_fiber_of_is_equiv,
    apply (to_is_equiv (arrow_equiv_arrow_right B (equiv.mk f H))),
  end

  definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ~ id)
    : is_contr (Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
  begin
    apply is_contr_equiv_closed_rev !sigma_pi_equiv_pi_sigma,
    apply is_contr_equiv_closed,
    { apply pi_equiv_pi_right, intro a,
      apply (fiber_eq_equiv (fiber.mk (u.1 (f a)) (u.2 (f a))) (fiber.mk a idp)) },
    exact _
  end

  omit H

  protected definition sigma_char : (is_equiv f) ≃
  (Σ(g : B → A) (ε : f ∘ g ~ id) (η : g ∘ f ~ id), Π(a : A), ε (f a) = ap f (η a)) :=
  equiv.MK (λH, ⟨inv f, right_inv f, left_inv f, adj f⟩)
           (λp, is_equiv.mk f p.1 p.2.1 p.2.2.1 p.2.2.2)
           (λp, begin
                  induction p with p1 p2,
                  induction p2 with p21 p22,
                  induction p22 with p221 p222,
                  reflexivity
                end)
           (λH, by induction H; reflexivity)

  protected definition sigma_char' : (is_equiv f) ≃
  (Σ(u : Σ(g : B → A), f ∘ g ~ id) (η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a)) :=
  calc
    (is_equiv f) ≃
      (Σ(g : B → A) (ε : f ∘ g ~ id) (η : g ∘ f ~ id), Π(a : A), ε (f a) = ap f (η a))
          : is_equiv.sigma_char
    ... ≃ (Σ(u : Σ(g : B → A), f ∘ g ~ id), Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a))
          : sigma_assoc_equiv (λu, Σ(η : u.1 ∘ f ~ id), Π(a : A), u.2 (f a) = ap f (η a))

  local attribute is_contr_right_inverse [instance] [priority 1600]
  local attribute is_contr_right_coherence [instance] [priority 1600]

  theorem is_prop_is_equiv [instance] : is_prop (is_equiv f) :=
  is_prop_of_imp_is_contr
    (λ(H : is_equiv f), is_contr_equiv_closed (equiv.symm !is_equiv.sigma_char') _)

  definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'}
    (p : f = f') : f⁻¹ = f'⁻¹ :=
  apd011 inv p !is_prop.elimo

  /- contractible fibers -/
  definition is_contr_fun_of_is_equiv [H : is_equiv f] : is_contr_fun f :=
  is_contr_fiber_of_is_equiv f

  definition is_prop_is_contr_fun (f : A → B) : is_prop (is_contr_fun f) := _

  definition is_equiv_of_is_contr_fun [H : is_contr_fun f] : is_equiv f :=
  adjointify _ (λb, point (center (fiber f b)))
               (λb, point_eq (center (fiber f b)))
               (λa, ap point (center_eq (fiber.mk a idp)))

  definition is_equiv_of_imp_is_equiv (H : B → is_equiv f) : is_equiv f :=
  @is_equiv_of_is_contr_fun _ _ f (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _)

  definition is_equiv_equiv_is_contr_fun : is_equiv f ≃ is_contr_fun f :=
  equiv_of_is_prop _ (λH, !is_equiv_of_is_contr_fun)

  theorem inv_commute'_fn {A : Type} {B C : A → Type} (f : Π{a}, B a → C a) [H : Πa, is_equiv (@f a)]
    {g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a))
    (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (b : B a) :
    inv_commute' @f @h @h' p (f b)
      = (ap f⁻¹ (p b))⁻¹ ⬝ left_inv f (h b) ⬝ (ap h (left_inv f b))⁻¹ :=
  begin
    rewrite [↑[inv_commute',inj'],+ap_con,-adj_inv f,+con.assoc,inv_con_cancel_left,
       adj f,+ap_inv,-+ap_compose,
       eq_bot_of_square (natural_square_tr (λb, (left_inv f (h b))⁻¹ ⬝ ap f⁻¹ (p b)) (left_inv f b))⁻¹ʰ,
       con_inv,inv_inv,+con.assoc],
    do 3 apply whisker_left,
    rewrite [con_inv_cancel_left,con.left_inv]
  end

end is_equiv

/- Moving equivalences around in homotopies -/
namespace is_equiv
  variables {A B C : Type} (f : A → B) [Hf : is_equiv f]

  include Hf

  section pre_compose
    variables (α : A → C) (β : B → C)

    -- homotopy_inv_of_homotopy_pre is in init.equiv
    protected definition inv_homotopy_of_homotopy_pre.is_equiv
      : is_equiv (inv_homotopy_of_homotopy_pre f α β) :=
    adjointify _ (homotopy_of_inv_homotopy_pre f α β)
    abstract begin
      intro q, apply eq_of_homotopy, intro b,
      unfold inv_homotopy_of_homotopy_pre,
      unfold homotopy_of_inv_homotopy_pre,
      apply inverse, apply eq_bot_of_square,
      apply eq_hconcat (ap02 α (adj_inv f b)),
      apply eq_hconcat (ap_compose α f⁻¹ (right_inv f b))⁻¹,
      apply natural_square q (right_inv f b)
    end end
    abstract begin
      intro p, apply eq_of_homotopy, intro a,
      unfold inv_homotopy_of_homotopy_pre,
      unfold homotopy_of_inv_homotopy_pre,
      apply trans (con.assoc
        (ap α (left_inv f a))⁻¹
        (p (f⁻¹ (f a)))
        (ap β (right_inv f (f a))))⁻¹,
      apply inverse, apply eq_bot_of_square,
      refine hconcat_eq _ (ap02 β (adj f a))⁻¹,
      refine hconcat_eq _ (ap_compose β f (left_inv f a)),
      apply natural_square p (left_inv f a)
    end end
  end pre_compose

  section post_compose
    variables (α : C → A) (β : C → B)

    -- homotopy_inv_of_homotopy_post is in init.equiv
    protected definition inv_homotopy_of_homotopy_post.is_equiv
      : is_equiv (inv_homotopy_of_homotopy_post f α β) :=
    adjointify _ (homotopy_of_inv_homotopy_post f α β)
    abstract begin
      intro q, apply eq_of_homotopy, intro c,
      unfold inv_homotopy_of_homotopy_post,
      unfold homotopy_of_inv_homotopy_post,
      apply trans (whisker_right (left_inv f (α c))
       (ap_con f⁻¹ (right_inv f (β c))⁻¹ (ap f (q c))
       ⬝ whisker_right (ap f⁻¹ (ap f (q c)))
       (ap_inv f⁻¹ (right_inv f (β c))))),
      apply inverse, apply eq_bot_of_square,
      apply eq_hconcat (adj_inv f (β c))⁻¹,
      apply eq_vconcat (ap_compose f⁻¹ f (q c))⁻¹,
      refine vconcat_eq _ (ap_id (q c)),
      apply natural_square_tr (left_inv f) (q c)
    end end
    abstract begin
      intro p, apply eq_of_homotopy, intro c,
      unfold inv_homotopy_of_homotopy_post,
      unfold homotopy_of_inv_homotopy_post,
      apply trans (whisker_left (right_inv f (β c))⁻¹
        (ap_con f (ap f⁻¹ (p c)) (left_inv f (α c)))),
      apply trans (con.assoc (right_inv f (β c))⁻¹ (ap f (ap f⁻¹ (p c)))
        (ap f (left_inv f (α c))))⁻¹,
      apply inverse, apply eq_bot_of_square,
      refine hconcat_eq _ (adj f (α c)),
      apply eq_vconcat (ap_compose f f⁻¹ (p c))⁻¹,
      refine vconcat_eq _ (ap_id (p c)),
      apply natural_square_tr (right_inv f) (p c)
    end end

  end post_compose

end is_equiv

namespace is_equiv

  /- Theorem 4.7.7 -/
  variables {A : Type} {P Q : A → Type}
  variable (f : Πa, P a → Q a)

  definition is_fiberwise_equiv [reducible] := Πa, is_equiv (f a)

  definition is_equiv_total_of_is_fiberwise_equiv [H : is_fiberwise_equiv f] : is_equiv (total f) :=
  is_equiv_sigma_functor id f

  definition is_fiberwise_equiv_of_is_equiv_total [H : is_equiv (total f)]
    : is_fiberwise_equiv f :=
  begin
    intro a,
    apply is_equiv_of_is_contr_fun, intro q,
    exact is_contr_equiv_closed (fiber_total_equiv f q) _
  end

end is_equiv

namespace equiv
  open is_equiv
  variables {A B C : Type}

  definition equiv_mk_eq {f f' : A → B} [H : is_equiv f] [H' : is_equiv f'] (p : f = f')
      : equiv.mk f H = equiv.mk f' H' :=
  apd011 equiv.mk p !is_prop.elimo

  definition equiv_eq' {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' :=
  by (cases f; cases f'; apply (equiv_mk_eq p))

  definition equiv_eq {f f' : A ≃ B} (p : to_fun f ~ to_fun f') : f = f' :=
  by apply equiv_eq'; apply eq_of_homotopy p

  definition ap_equiv_eq {X Y : Type} {e e' : X ≃ Y} (p : e ~ e') (x : X) :
    ap (λ(e : X ≃ Y), e x) (equiv_eq p) = p x :=
  begin
    cases e with e He, cases e' with e' He', esimp at *, esimp [equiv_eq],
    refine homotopy.rec_on' p _, intro q, induction q, esimp [equiv_eq', equiv_mk_eq],
    assert H : He = He', apply is_prop.elim, induction H, rewrite [is_prop_elimo_self]
  end

  definition trans_symm (f : A ≃ B) (g : B ≃ C) : (f ⬝e g)⁻¹ᵉ = g⁻¹ᵉ ⬝e f⁻¹ᵉ :> (C ≃ A) :=
  equiv_eq' idp

  definition symm_symm (f : A ≃ B) : f⁻¹ᵉ⁻¹ᵉ = f :> (A ≃ B) :=
  equiv_eq' idp

  protected definition equiv.sigma_char [constructor]
    (A B : Type) : (A ≃ B) ≃ Σ(f : A → B), is_equiv f :=
  begin
    fapply equiv.MK,
      {intro F, exact ⟨to_fun F, to_is_equiv F⟩},
      {intro p, cases p with f H, exact (equiv.mk f H)},
      {intro p, cases p, exact idp},
      {intro F, cases F, exact idp},
  end

  definition equiv_eq_char (f f' : A ≃ B) : (f = f') ≃ (to_fun f = to_fun f') :=
  calc
    (f = f') ≃ (!equiv.sigma_char f = !equiv.sigma_char f')
                : eq_equiv_fn_eq !equiv.sigma_char
         ... ≃ ((to_fun !equiv.sigma_char f).1 = (to_fun !equiv.sigma_char f').1 ) : equiv_subtype
         ... ≃ (to_fun f = to_fun f') : equiv.rfl

  definition is_equiv_ap_to_fun (f f' : A ≃ B)
    : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') :=
  begin
    fapply adjointify,
      {intro p, cases f with f H, cases f' with f' H', cases p, apply ap (mk f'), apply is_prop.elim},
      {intro p, cases f with f H, cases f' with f' H', cases p,
        apply @concat _ _ (ap to_fun (ap (equiv.mk f') (is_prop.elim H H'))), {apply idp},
        generalize is_prop.elim H H', intro q, cases q, apply idp},
      {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_set.elim}
  end

  definition equiv_pathover {A : Type} {a a' : A} (p : a = a')
    {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
    (r : to_fun f =[p] to_fun g) : f =[p] g :=
  begin
    fapply pathover_of_fn_pathover_fn,
    { intro a, apply equiv.sigma_char },
    { apply sigma_pathover _ _ _ r, apply is_prop.elimo }
  end

  definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a')
    {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
    (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g :=
  begin
    apply equiv_pathover, apply arrow_pathover, exact r
  end

  definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a')
    {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
    (r : to_inv f =[p] to_inv g) : f =[p] g :=
  begin
    /- this proof is a bit weird, but it works -/
    apply equiv_pathover,
    change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ,
    apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ),
    apply equiv_pathover,
    exact r
  end

  definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) :=
  begin
    apply @is_contr_of_inhabited_prop, apply is_prop.mk,
    intro x y, cases x with fx Hx, cases y with fy Hy, generalize Hy,
    apply (eq_of_homotopy (λ a, !eq_of_is_contr)) ▸ (λ Hy, !is_prop.elim ▸ rfl),
    apply equiv_of_is_contr_of_is_contr
  end

  definition is_trunc_succ_equiv (n : trunc_index) (A B : Type)
  [HA : is_trunc n.+1 A] [HB : is_trunc n.+1 B] : is_trunc n.+1 (A ≃ B) :=
  @is_trunc_equiv_closed _ _ n.+1 (equiv.symm !equiv.sigma_char)
  (@is_trunc_sigma _ _ _ _ (λ f, !is_trunc_succ_of_is_prop))

  definition is_trunc_equiv (n : trunc_index) (A B : Type)
  [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) :=
  by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv

  definition inj'_idp {A B : Type} (f : A → B) [is_equiv f] (x : A)
    : inj' f (idpath (f x)) = idpath x :=
  !con.left_inv

  definition inj'_con {A B : Type} (f : A → B) [is_equiv f] {x y z : A}
    (p : f x = f y) (q : f y = f z)
    : inj' f (p ⬝ q) = inj' f p ⬝ inj' f q :=
  begin
    unfold inj',
    refine _ ⬝ !con.assoc, apply whisker_right,
    refine _ ⬝ !con.assoc⁻¹ ⬝ !con.assoc⁻¹, apply whisker_left,
    refine !ap_con ⬝ _, apply whisker_left,
    refine !con_inv_cancel_left⁻¹
  end

end equiv