f513538631
remove funext class, remove a couple of sorry's, add characterization of equality in trunctypes, use Jeremy's format for headers everywhere in the HoTT library, continue working on Yoneda embedding
267 lines
11 KiB
Text
267 lines
11 KiB
Text
/-
|
||
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] `⁻¹ᵉ`:100 := 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
|
||
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 (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 (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_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
|
||
calc_trans equiv.trans
|
||
calc_refl equiv.refl
|
||
calc_symm equiv.symm
|
||
|
||
end equiv
|