lean2/library/hott/funext_from_ua.lean

105 lines
4 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 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
import hott.axioms.ua hott.equiv hott.equiv_precomp hott.funext_varieties
import data.prod data.sigma data.unit
open path function prod sigma truncation Equiv unit
-- First, define an axiom free variant of Univalence
definition ua_type := Π (A B : Type), IsEquiv (equiv_path A B)
context
parameters {ua : ua_type}
-- TODO base this theorem on UA instead of FunExt.
-- IsEquiv.postcompose relies on FunExt!
protected theorem ua_isequiv_postcompose {A B C : Type} {w : A → B} {H0 : IsEquiv w}
: IsEquiv (@compose C A B w) :=
!IsEquiv.postcompose
-- We are ready to prove functional extensionality,
-- starting with the naive non-dependent version.
protected definition diagonal [reducible] (B : Type) : Type
:= Σ xy : B × B, pr₁ xy ≈ pr₂ xy
protected definition isequiv_src_compose {A B C : Type}
: @IsEquiv (A → diagonal B)
(A → B)
(compose (pr₁ ∘ dpr1))
:= @ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1)
(IsEquiv.adjointify (pr₁ ∘ dpr1)
(λ x, dpair (x , x) idp) (λx, idp)
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
(λ b c p, path.rec_on p idp))))
protected definition isequiv_tgt_compose {A B C : Type}
: @IsEquiv (A → diagonal B)
(A → B)
(compose (pr₂ ∘ dpr1))
:= @ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1)
(IsEquiv.adjointify (pr2 ∘ dpr1)
(λ x, dpair (x , x) idp) (λx, idp)
(λ x, sigma.rec_on x
(λ xy, prod.rec_on xy
(λ b c p, path.rec_on p idp))))
theorem ua_implies_funext_nondep {A B : Type}
: Π {f g : A → B}, f g → f ≈ g
:= (λ (f g : A → B) (p : f g),
let d := λ (x : A), dpair (f x , f x) idp in
let e := λ (x : A), dpair (f x , g x) (p x) in
let precomp1 := compose (pr₁ ∘ dpr1) in
have equiv1 [visible] : IsEquiv precomp1,
from @isequiv_src_compose A B (diagonal B),
have equiv2 [visible] : Π x y, IsEquiv (ap precomp1),
from IsEquiv.ap_closed precomp1,
have H' : Π (x y : A → diagonal B),
pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y,
from (λ x y, IsEquiv.inv (ap precomp1)),
have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e,
from idp,
have eq0 : d ≈ e,
from H' d e eq2,
have eq1 : (pr₂ ∘ dpr1) ∘ d ≈ (pr₂ ∘ dpr1) ∘ e,
from ap _ eq0,
eq1
)
end
context
universe l
parameters {ua1 ua2 : ua_type.{1}}
-- Now we use this to prove weak funext, which as we know
-- implies (with dependent eta) also the strong dependent funext.
theorem ua_implies_weak_funext : weak_funext
:= (λ A P allcontr,
let U := (λ (x : A), unit) in
have pequiv : Πx, P x ≃ U x,
from (λ x, @equiv_contr_unit (P x) (allcontr x)),
have psim : Πx, P x ≈ U x,
from (λ x, @IsEquiv.inv _ _
(equiv_path.{1} (P x) (U x)) (ua1 (P x) (U x)) (pequiv x)),
have p : P ≈ U,
from ua_implies_funext_nondep psim,
have tU' : is_contr (A → unit),
from is_contr.mk (λ x, ⋆)
(λ f, ua_implies_funext_nondep
(λ x, unit.rec_on (f x) idp)),
have tU : is_contr (Πx, U x),
from tU',
have tlast : is_contr (Πx, P x),
from path.transport _ (p⁻¹) tU,
tlast
)
end
-- In the following we will proof function extensionality using the univalence axiom
-- TODO: check out why I have to generalize on A and P here
definition ua_implies_funext_type {ua : ua_type.{1}} : @funext_type :=
(λ A P, weak_funext_implies_funext (@ua_implies_weak_funext ua))