lean2/hott/init/axioms/funext_of_ua.hlean

131 lines
5 KiB
Text
Raw Normal View History

2014-12-12 04:14:53 +00:00
-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Jakob von Raumer
-- Ported from Coq HoTT
2014-12-12 18:17:50 +00:00
prelude
2014-12-16 20:10:12 +00:00
import ..equiv ..datatypes ..types.prod
2014-12-12 18:17:50 +00:00
import .funext_varieties .ua .funext
2014-12-12 04:14:53 +00:00
open eq function prod is_trunc sigma equiv is_equiv unit
2014-12-12 04:14:53 +00:00
context
universe variables l
private theorem ua_isequiv_postcompose {A B : Type.{l}} {C : Type}
{w : A → B} [H0 : is_equiv w] : is_equiv (@compose C A B w) :=
2014-12-12 04:14:53 +00:00
let w' := equiv.mk w H0 in
let eqinv : A = B := ((@is_equiv.inv _ _ _ (univalence A B)) w') in
let eq' := equiv_of_eq eqinv in
2014-12-12 04:14:53 +00:00
is_equiv.adjointify (@compose C A B w)
(@compose C B A (is_equiv.inv w))
(λ (x : C → B),
2014-12-12 18:17:50 +00:00
have eqretr : eq' = w',
from (@retr _ _ (@equiv_of_eq A B) (univalence A B) w'),
2014-12-12 18:17:50 +00:00
have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹,
2014-12-12 04:14:53 +00:00
from inv_eq eq' w' eqretr,
2014-12-12 18:17:50 +00:00
have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
2014-12-12 04:14:53 +00:00
from (λ p,
(@eq.rec_on Type.{l} A
(λ B' p', Π (x' : C → B'), (to_fun (equiv_of_eq p'))
∘ ((to_fun (equiv_of_eq p'))⁻¹ ∘ x') = x')
2014-12-12 04:14:53 +00:00
B p (λ x', idp))
) eqinv x,
2014-12-12 18:17:50 +00:00
have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) = x,
2014-12-12 04:14:53 +00:00
from eqretr ▹ eqfin,
2014-12-12 18:17:50 +00:00
have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) = x,
2014-12-12 04:14:53 +00:00
from invs_eq ▹ eqfin',
eqfin''
)
(λ (x : C → A),
2014-12-12 18:17:50 +00:00
have eqretr : eq' = w',
from (@retr _ _ (@equiv_of_eq A B) (univalence A B) w'),
2014-12-12 18:17:50 +00:00
have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹,
2014-12-12 04:14:53 +00:00
from inv_eq eq' w' eqretr,
2014-12-12 18:17:50 +00:00
have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) = x,
from (λ p, eq.rec_on p idp) eqinv,
have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) = x,
2014-12-12 04:14:53 +00:00
from eqretr ▹ eqfin,
2014-12-12 18:17:50 +00:00
have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) = x,
2014-12-12 04:14:53 +00:00
from invs_eq ▹ eqfin',
eqfin''
)
-- We are ready to prove functional extensionality,
-- starting with the naive non-dependent version.
private definition diagonal [reducible] (B : Type) : Type
2014-12-12 18:17:50 +00:00
:= Σ xy : B × B, pr₁ xy = pr₂ xy
2014-12-12 04:14:53 +00:00
private definition isequiv_src_compose {A B : Type}
2014-12-12 04:14:53 +00:00
: @is_equiv (A → diagonal B)
(A → B)
(compose (pr₁ ∘ pr1)) :=
@ua_isequiv_postcompose _ _ _ (pr₁ ∘ pr1)
(is_equiv.adjointify (pr₁ ∘ pr1)
(λ x, sigma.mk (x , x) idp) (λx, idp)
2014-12-12 04:14:53 +00:00
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
2014-12-12 18:17:50 +00:00
(λ b c p, eq.rec_on p idp))))
2014-12-12 04:14:53 +00:00
private definition isequiv_tgt_compose {A B : Type}
2014-12-12 04:14:53 +00:00
: @is_equiv (A → diagonal B)
(A → B)
(compose (pr₂ ∘ pr1)) :=
@ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1)
(is_equiv.adjointify (pr2 ∘ pr1)
(λ x, sigma.mk (x , x) idp) (λx, idp)
2014-12-12 04:14:53 +00:00
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
2014-12-12 18:17:50 +00:00
(λ b c p, eq.rec_on p idp))))
2014-12-12 04:14:53 +00:00
set_option class.conservative false
theorem nondep_funext_from_ua {A : Type} {B : Type}
2014-12-12 18:17:50 +00:00
: Π {f g : A → B}, f g → f = g :=
2014-12-12 04:14:53 +00:00
(λ (f g : A → B) (p : f g),
let d := λ (x : A), sigma.mk (f x , f x) idp in
let e := λ (x : A), sigma.mk (f x , g x) (p x) in
let precomp1 := compose (pr₁ ∘ pr1) in
2014-12-12 04:14:53 +00:00
have equiv1 [visible] : is_equiv precomp1,
from @isequiv_src_compose A B,
have equiv2 [visible] : Π x y, is_equiv (ap precomp1),
from is_equiv.is_equiv_ap precomp1,
2014-12-12 04:14:53 +00:00
have H' : Π (x y : A → diagonal B),
pr₁ ∘ pr1 ∘ x = pr₁ ∘ pr1 ∘ y → x = y,
2014-12-12 04:14:53 +00:00
from (λ x y, is_equiv.inv (ap precomp1)),
have eq2 : pr₁ ∘ pr1 ∘ d = pr₁ ∘ pr1 ∘ e,
2014-12-12 04:14:53 +00:00
from idp,
2014-12-12 18:17:50 +00:00
have eq0 : d = e,
2014-12-12 04:14:53 +00:00
from H' d e eq2,
have eq1 : (pr₂ ∘ pr1) ∘ d = (pr₂ ∘ pr1) ∘ e,
2014-12-12 04:14:53 +00:00
from ap _ eq0,
eq1
)
end
-- Now we use this to prove weak funext, which as we know
-- implies (with dependent eta) also the strong dependent funext.
theorem weak_funext_of_ua : weak_funext :=
2014-12-12 04:14:53 +00:00
(λ (A : Type) (P : A → Type) allcontr,
let U := (λ (x : A), unit) in
have pequiv : Π (x : A), P x ≃ U x,
from (λ x, @equiv_unit_of_is_contr (P x) (allcontr x)),
2014-12-12 18:17:50 +00:00
have psim : Π (x : A), P x = U x,
2014-12-12 04:14:53 +00:00
from (λ x, @is_equiv.inv _ _
equiv_of_eq (univalence _ _) (pequiv x)),
2014-12-12 18:17:50 +00:00
have p : P = U,
from @nondep_funext_from_ua A Type P U psim,
2014-12-12 04:14:53 +00:00
have tU' : is_contr (A → unit),
from is_contr.mk (λ x, ⋆)
(λ f, @nondep_funext_from_ua A unit (λ x, ⋆) f
2014-12-12 04:14:53 +00:00
(λ x, unit.rec_on (f x) idp)),
have tU : is_contr (Π x, U x),
from tU',
have tlast : is_contr (Πx, P x),
2014-12-12 18:17:50 +00:00
from eq.transport _ (p⁻¹) tU,
2014-12-12 04:14:53 +00:00
tlast
)
-- In the following we will proof function extensionality using the univalence axiom
definition funext_of_ua [instance] : funext :=
funext_of_weak_funext (@weak_funext_of_ua)