122 lines
4.8 KiB
Text
122 lines
4.8 KiB
Text
/-
|
||
Copyright (c) 2014 Floris van Doorn. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Author: Floris van Doorn
|
||
Ported from Coq HoTT
|
||
|
||
Theorems about pi-types (dependent function spaces)
|
||
-/
|
||
import types.sigma
|
||
|
||
open eq equiv is_equiv funext
|
||
|
||
namespace pi
|
||
universe variables l k
|
||
variables {A A' : Type.{l}} {B : A → Type.{k}} {B' : A' → Type.{k}} {C : Πa, B a → Type}
|
||
{D : Πa b, C a b → Type}
|
||
{a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a}
|
||
|
||
/- Paths -/
|
||
|
||
/- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g].
|
||
|
||
This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path: -/
|
||
|
||
/- Now we show how these things compute. -/
|
||
|
||
definition apD10_path_pi [H : funext] (h : f ∼ g) : apD10 (path_pi h) ∼ h :=
|
||
apD10 (retr apD10 h)
|
||
|
||
definition path_pi_eta [H : funext] (p : f = g) : path_pi (apD10 p) = p :=
|
||
sect apD10 p
|
||
|
||
definition path_pi_idp [H : funext] : path_pi (λx : A, refl (f x)) = refl f :=
|
||
!path_pi_eta
|
||
|
||
/- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
|
||
|
||
definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f = g) ≃ (f ∼ g) :=
|
||
equiv.mk _ !funext.ap
|
||
|
||
definition is_equiv_path_pi [instance] [H : funext] (f g : Πx, B x)
|
||
: is_equiv (@path_pi _ _ _ f g) :=
|
||
inv_closed apD10
|
||
|
||
definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f = g) :=
|
||
equiv.mk _ !is_equiv_path_pi
|
||
|
||
|
||
/- Transport -/
|
||
|
||
protected definition transport (p : a = a') (f : Π(b : B a), C a b)
|
||
: (transport (λa, Π(b : B a), C a b) p f)
|
||
∼ (λb, transport (C a') !transport_pV (transportD _ _ p _ (f (p⁻¹ ▹ b)))) :=
|
||
eq.rec_on p (λx, idp)
|
||
|
||
/- A special case of [transport_pi] where the type [B] does not depend on [A],
|
||
and so it is just a fixed type [B]. -/
|
||
definition transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b)
|
||
: (eq.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, eq.transport (λa, C a b) p (f b)) :=
|
||
eq.rec_on p (λx, idp)
|
||
|
||
/- Maps on paths -/
|
||
|
||
/- The action of maps given by lambda. -/
|
||
definition ap_lambdaD [H : funext] {C : A' → Type} (p : a = a') (f : Πa b, C b) :
|
||
ap (λa b, f a b) p = path_pi (λb, ap (λa, f a b) p) :=
|
||
begin
|
||
apply (eq.rec_on p),
|
||
apply inverse,
|
||
apply path_pi_idp
|
||
end
|
||
|
||
/- Dependent paths -/
|
||
|
||
/- with more implicit arguments the conclusion of the following theorem is
|
||
(Π(b : B a), transportD B C p b (f b) = g (eq.transport B p b)) ≃
|
||
(eq.transport (λa, Π(b : B a), C a b) p f = g) -/
|
||
definition dpath_pi [H : funext] (p : a = a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
|
||
: (Π(b : B a), p ▹D (f b) = g (p ▹ b)) ≃ (p ▹ f = g) :=
|
||
eq.rec_on p (λg, !homotopy_equiv_path) g
|
||
|
||
section open sigma sigma.ops
|
||
/- more implicit arguments:
|
||
(Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃
|
||
(Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/
|
||
definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a = a')
|
||
(f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
|
||
(Π(b : B a), (sigma.path p idp) ▹ (f b) = g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) = g (p ▹ b)) :=
|
||
eq.rec_on p (λg, !equiv.refl) g
|
||
end
|
||
|
||
variables (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
|
||
|
||
definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
|
||
p⁻¹ ▹ u
|
||
|
||
protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
|
||
/- Equivalences -/
|
||
definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')
|
||
[H0 : is_equiv f0] [H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')]
|
||
: is_equiv (functor_pi f0 f1) :=
|
||
begin
|
||
apply (adjointify (functor_pi f0 f1) (functor_pi (f0⁻¹)
|
||
(λ(a : A) (b' : B' (f0⁻¹ a)), transport B (retr f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
|
||
intro h, apply path_pi,
|
||
esimp {functor_pi, function.compose}, -- simplify (and unfold function_pi and function.compose)
|
||
--first subgoal
|
||
intro a', esimp,
|
||
rewrite adj,
|
||
rewrite -transport_compose,
|
||
rewrite {f1 a' _}(ap_transport _ f1 _),
|
||
apply (transport_V (λx, sect f0 a' ▹ x = h a') (retr (f1 _) _)),
|
||
-- retr cannot be used as rewrite rule, the resulting type is not an equality
|
||
apply apD,
|
||
intro h, beta,
|
||
apply path_pi, intro a, esimp,
|
||
apply (transport_V (λx, retr f0 a ▹ x = h a) (sect (f1 _) _)),
|
||
esimp {function.id},
|
||
apply apD
|
||
end
|
||
|
||
end pi
|