lean2/hott/init/axioms/funext_varieties.hlean

106 lines
4.2 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.
-- Authors: Jakob von Raumer
-- Ported from Coq HoTT
2014-12-16 20:10:12 +00:00
prelude
2014-12-12 18:17:50 +00:00
import ..path ..trunc ..equiv .funext
2014-12-12 04:14:53 +00:00
open eq is_trunc sigma function
2014-12-12 04:14:53 +00:00
/- In hott.axioms.funext, we defined function extensionality to be the assertion
that the map apD10 is an equivalence. We now prove that this follows
from a couple of weaker-looking forms of function extensionality. We do
require eta conversion, which Coq 8.4+ has judgmentally.
This proof is originally due to Voevodsky; it has since been simplified
by Peter Lumsdaine and Michael Shulman. -/
-- Naive funext is the simple assertion that pointwise equal functions are equal.
-- TODO think about universe levels
definition naive_funext :=
2014-12-12 18:17:50 +00:00
Π {A : Type} {P : A → Type} (f g : Πx, P x), (f g) → f = g
2014-12-12 04:14:53 +00:00
-- Weak funext says that a product of contractible types is contractible.
definition weak_funext :=
Π {A : Type} (P : A → Type) [H: Πx, is_contr (P x)], is_contr (Πx, P x)
2014-12-12 04:14:53 +00:00
-- The obvious implications are Funext -> NaiveFunext -> WeakFunext
-- TODO: Get class inference to work locally
definition naive_funext_from_funext [F : funext] : naive_funext :=
(λ A P f g h, funext.eq_of_homotopy h)
2014-12-12 04:14:53 +00:00
definition weak_funext_of_naive_funext : naive_funext → weak_funext :=
2014-12-12 04:14:53 +00:00
(λ nf A P (Pc : Πx, is_contr (P x)),
let c := λx, center (P x) in
is_contr.mk c (λ f,
have eq' : (λx, center (P x)) f,
from (λx, contr (f x)),
2014-12-12 18:17:50 +00:00
have eq : (λx, center (P x)) = f,
2014-12-12 04:14:53 +00:00
from nf A P (λx, center (P x)) f eq',
eq
)
)
/- The less obvious direction is that WeakFunext implies Funext
(and hence all three are logically equivalent). The point is that under weak
funext, the space of "pointwise homotopies" has the same universal property as
the space of paths. -/
context
universes l k
parameters (wf : weak_funext.{l k}) {A : Type.{l}} {B : A → Type.{k}} (f : Π x, B x)
2014-12-12 04:14:53 +00:00
definition is_contr_sigma_homotopy [instance] : is_contr (Σ (g : Π x, B x), f g) :=
is_contr.mk (sigma.mk f (homotopy.refl f))
2014-12-12 04:14:53 +00:00
(λ dp, sigma.rec_on dp
(λ (g : Π x, B x) (h : f g),
2014-12-12 18:17:50 +00:00
let r := λ (k : Π x, Σ y, f x = y),
@sigma.mk _ (λg, f g)
(λx, pr1 (k x)) (λx, pr2 (k x)) in
let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in
2014-12-12 18:17:50 +00:00
have t1 : Πx, is_contr (Σ y, f x = y),
from (λx, !is_contr_sigma_eq),
2014-12-12 18:17:50 +00:00
have t2 : is_contr (Πx, Σ y, f x = y),
2014-12-12 04:14:53 +00:00
from !wf,
have t3 : (λ x, @sigma.mk _ (λ y, f x = y) (f x) idp) = s g h,
from @center_eq (Π x, Σ y, f x = y) t2 _ _,
have t4 : r (λ x, sigma.mk (f x) idp) = r (s g h),
2014-12-12 04:14:53 +00:00
from ap r t3,
have endt : sigma.mk f (homotopy.refl f) = sigma.mk g h,
2014-12-12 04:14:53 +00:00
from t4,
endt
)
)
parameters (Q : Π g (h : f g), Type) (d : Q f (homotopy.refl f))
2014-12-12 04:14:53 +00:00
definition homotopy_ind (g : Πx, B x) (h : f g) : Q g h :=
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h)
(@center_eq _ is_contr_sigma_homotopy _ _) d
2014-12-12 04:14:53 +00:00
local attribute homotopy_ind [reducible]
definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
(@hprop_eq _ _ _ _ !center_eq idp)⁻¹ ▹ idp
2014-12-12 04:14:53 +00:00
end
-- Now the proof is fairly easy; we can just use the same induction principle on both sides.
universe variables l k
theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} :=
2014-12-12 04:14:53 +00:00
funext.mk (λ A B f g,
2014-12-12 18:17:50 +00:00
let eq_to_f := (λ g' x, f = g') in
let sim2path := homotopy_ind _ f eq_to_f idp in
have t1 : sim2path f (homotopy.refl f) = idp,
proof homotopy_ind_comp _ f eq_to_f idp qed,
have t2 : apD10 (sim2path f (homotopy.refl f)) = (homotopy.refl f),
2014-12-12 04:14:53 +00:00
proof ap apD10 t1 qed,
have sect : apD10 ∘ (sim2path g) id,
proof (homotopy_ind _ f (λ g' x, apD10 (sim2path g' x) = x) t2) g qed,
2014-12-12 04:14:53 +00:00
have retr : (sim2path g) ∘ apD10 id,
from (λ h, eq.rec_on h (homotopy_ind_comp _ f _ idp)),
2014-12-12 04:14:53 +00:00
is_equiv.adjointify apD10 (sim2path g) sect retr)
definition funext_from_naive_funext : naive_funext -> funext :=
compose funext_of_weak_funext weak_funext_of_naive_funext