lean2/hott/init/equiv.hlean
2015-03-04 00:17:41 -05:00

275 lines
11 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
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
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ᵉ`:std.prec.max_plus := inv
section
variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
-- The identity function is an equivalence.
-- TODO: make A explicit
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.right_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.left_inv _
⬝ !idp_con)
(λp, whisker_right (whisker_left _ (ap_compose f f⁻¹ _)⁻¹) _
⬝ con_ap_con_eq_con_con (sect f) _ _
⬝ whisker_right !con.left_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
namespace ops
attribute to_fun [coercion]
end ops
open equiv.ops
attribute to_is_equiv [instance]
infix `≃`:25 := equiv
variables {A B C : Type}
protected definition MK [reducible] (f : A → B) (g : B → A)
(retr : f ∘ g id) (sect : g ∘ f id) : A ≃ B :=
equiv.mk f (adjointify f g retr sect)
definition to_inv [reducible] (f : A ≃ B) : B → A :=
f⁻¹
protected definition refl : A ≃ A :=
equiv.mk id !is_equiv_id
protected definition symm (f : A ≃ B) : B ≃ A :=
equiv.mk f⁻¹ !is_equiv_inv
protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
equiv.mk (g ∘ f) !is_equiv_compose
definition equiv_of_eq_fn_of_equiv (f : A ≃ B) (f' : A → B) (Heq : f = f') : A ≃ B :=
equiv.mk f' (is_equiv_eq_closed f Heq)
definition eq_equiv_fn_eq (f : A → B) [H : is_equiv f] (a b : A) : (a = b) ≃ (f a = f b) :=
equiv.mk (ap f) !is_equiv_ap
definition eq_equiv_fn_eq_of_equiv (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) :=
equiv.mk (ap f) !is_equiv_ap
definition equiv_ap (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) :=
equiv.mk (transport P p) !is_equiv_tr
--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
definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▹ q
definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▹ p
calc_trans equiv.trans
calc_refl equiv.refl
calc_symm equiv.symm
calc_trans equiv_of_equiv_of_eq
calc_trans equiv_of_eq_of_equiv
end equiv