michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott/types/sigma): port large part of the sigma library from the hott library

Browse source 
most importantly, prove the characterization of paths in sigma types
This commit is contained in:
Floris van Doorn 2014-11-09 17:22:42 -05:00 committed by Leonardo de Moura
parent 919007612a
commit e8b076e460
5 changed files with 323 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

33
library/data/sigma/thms.lean
View file

@ -5,9 +5,23 @@ import data.sigma.decl
open inhabited eq.ops
namespace sigma
notation `dpr₁` := dpr1
notation `dpr₂` := dpr2
namespace ops
postfix `.1`:10000 := dpr1
postfix `.2`:10000 := dpr2
notation `(` t:(foldr `;`:0 (e r, sigma.dpair e r)) `)` := t
end ops
open ops
universe variables u v
variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
definition unpack {C : (Σa, B a) → Type} {u : Σa, B a} (H : C ( u.1 ; u.2)) : C u :=
destruct u (λx y H, H) H
theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
dpair a₁ b₁ = dpair a₂ b₂ :=
dcongr_arg2 dpair H₁ H₂
@ -34,24 +48,23 @@ namespace sigma
variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := dpair a (dpair b (dpair c d))
definition dtrip (a : A) (b : B a) (c : C a b) := (a; b; c)
definition dquad (a : A) (b : B a) (c : C a b) (d : D a b c) := (a; b; c; d)
definition dpr1' (x : Σ a, B a) := dpr1 x
definition dpr2' (x : Σ a b, C a b) := dpr1 (dpr2 x)
definition dpr3 (x : Σ a b, C a b) := dpr2 (dpr2 x)
definition dpr3' (x : Σ a b c, D a b c) := dpr1 (dpr2 (dpr2 x))
definition dpr4 (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
definition dpr1' (x : Σ a, B a) := x.1
definition dpr2' (x : Σ a b, C a b) := x.2.1
definition dpr3 (x : Σ a b, C a b) := x.2.2
definition dpr3' (x : Σ a b c, D a b c) := x.2.2.1
definition dpr4 (x : Σ a b c, D a b c) := x.2.2.2
theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
(H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
(a₁; b₁; c₁) = (a₂; b₂; c₂) :=
dcongr_arg3 dtrip H₁ H₂ H₃
theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
{c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
(H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) :
dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
(H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : (a₁; b₁; c₁) = (a₂; b₂; c₂) :=
hdcongr_arg3 dtrip H₁ (heq.from_eq H₂) H₃
theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :

6
library/hott/equiv.lean
View file

@ -243,7 +243,7 @@ namespace IsEquiv
end
--Transporting is an equivalence
definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) :=
protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (IsEquiv (transport P p)) :=
IsEquiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p)
end IsEquiv
@ -257,7 +257,7 @@ namespace Equiv
protected definition id : A ≃ A := Equiv.mk id IsEquiv.id_closed
theorem compose (eqg: B ≃ C) : A ≃ C :=
protected theorem compose (eqg: B ≃ C) : A ≃ C :=
Equiv.mk ((equiv_fun eqg) ∘ f)
(IsEquiv.comp_closed Hf (equiv_isequiv eqg))
@ -273,7 +273,7 @@ namespace Equiv
theorem cancel_L {g : C → A} (Hgf : IsEquiv (f ∘ g)) : C ≃ A :=
Equiv.mk g (IsEquiv.cancel_L f _)
theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
protected theorem transport (P : A → Type) {x y : A} {p : x ≈ y} : (P x) ≃ (P y) :=
Equiv.mk (transport P p) (IsEquiv.transport P p)
end

5
library/hott/path.lean
View file

@ -8,7 +8,7 @@
-- o Try doing these proofs with tactics.
-- o Try using the simplifier on some of these proofs.
import general_notation algebra.function tools.tactic
import general_notation type algebra.function tools.tactic
open function
@ -356,7 +356,7 @@ definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A}
begin
apply (rec_on s),
apply (rec_on q),
apply (concat_1p _ ▹ idp)
apply (concat_1p (p x) ▹ idp)
end
-- Action of [apD10] and [ap10] on paths
@ -477,6 +477,7 @@ definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p
rec_on r (concat_1p _)⁻¹
-- Transporting in a pulled back fibration.
-- TODO: P can probably be implicit
definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
transport (λx, P (f x)) p z ≈ transport P (ap f p) z :=
rec_on p idp

48
library/hott/trunc.lean
View file

@ -36,7 +36,7 @@ namespace truncation
end trunc_index
-- Coq calls this `-2+`, but `+2+` looks more natural, since trunc_index_add 0 0 = 2
infix `+2+`:65 := add
infix `+2+`:65 := trunc_index.add
notation x <= y := trunc_index.leq x y
notation x ≤ y := trunc_index.leq x y
@ -58,14 +58,14 @@ namespace truncation
use `is_trunc` and `is_contr`
-/
structure contr_internal (A : Type₊) :=
structure contr_internal (A : Type) :=
(center : A) (contr : Π(a : A), center ≈ a)
definition is_trunc_internal (n : trunc_index) : Type₊ → Type₊ :=
definition is_trunc_internal (n : trunc_index) : Type → Type :=
trunc_index.rec_on n (λA, contr_internal A)
(λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y)))
structure is_trunc [class] (n : trunc_index) (A : Type₊) :=
structure is_trunc [class] (n : trunc_index) (A : Type) :=
(to_internal : is_trunc_internal n A)
-- should this be notation or definitions?
@ -76,10 +76,10 @@ namespace truncation
-- definition is_hprop := is_trunc -1
-- definition is_hset := is_trunc 0
variables {A B : Type₊}
variables {A B : Type}
-- maybe rename to is_trunc_succ.mk
definition is_trunc_succ (A : Type₊) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)]
definition is_trunc_succ (A : Type) {n : trunc_index} [H : ∀x y : A, is_trunc n (x ≈ y)]
: is_trunc n.+1 A :=
is_trunc.mk (λ x y, is_trunc.to_internal)
@ -92,7 +92,7 @@ namespace truncation
definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A :=
is_trunc.mk (contr_internal.mk center contr)
definition center (A : Type₊) [H : is_contr A] : A :=
definition center (A : Type) [H : is_contr A] : A :=
@contr_internal.center A is_trunc.to_internal
definition contr [H : is_contr A] (a : A) : !center ≈ a :=
@ -101,17 +101,17 @@ namespace truncation
definition path_contr [H : is_contr A] (x y : A) : x ≈ y :=
contr x⁻¹ ⬝ (contr y)
definition path2_contr {A : Type₊} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
definition path2_contr {A : Type} [H : is_contr A] {x y : A} (p q : x ≈ y) : p ≈ q :=
have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp),
K p⁻¹ ⬝ K q
definition contr_paths_contr [instance] {A : Type₊} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
definition contr_paths_contr [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x ≈ y) :=
is_contr.mk !path_contr (λ p, !path2_contr)
/- truncation is upward close -/
-- n-types are also (n+1)-types
definition trunc_succ [instance] (A : Type₊) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
definition trunc_succ [instance] (A : Type) (n : trunc_index) [H : is_trunc n A] : is_trunc (n.+1) A :=
trunc_index.rec_on n
(λ A (H : is_contr A), !is_trunc_succ)
(λ n IH A (H : is_trunc (n.+1) A), @is_trunc_succ _ _ (λ x y, IH _ !succ_is_trunc))
@ -119,15 +119,15 @@ namespace truncation
--in the proof the type of H is given explicitly to make it available for class inference
definition trunc_leq (A : Type₊) (n m : trunc_index) (Hnm : n ≤ m)
definition trunc_leq (A : Type) (n m : trunc_index) (Hnm : n ≤ m)
[Hn : is_trunc n A] : is_trunc m A :=
have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
λ k A, trunc_index.cases_on k
(λh1 h2, h2)
(λk h1 h2, empty.elim (is_trunc -2 A) (trunc_index.not_succ_le_minus_two h1)),
have step : Π (m : trunc_index)
(IHm : Π (n : trunc_index) (A : Type₊), n ≤ m → is_trunc n A → is_trunc m A)
(n : trunc_index) (A : Type₊)
(IHm : Π (n : trunc_index) (A : Type), n ≤ m → is_trunc n A → is_trunc m A)
(n : trunc_index) (A : Type)
(Hnm : n ≤ m .+1) (Hn : is_trunc n A), is_trunc m .+1 A, from
λm IHm n, trunc_index.rec_on n
(λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn))
@ -136,14 +136,14 @@ namespace truncation
trunc_index.rec_on m base step n A Hnm Hn
-- the following cannot be instances in their current form, because it is looping
definition trunc_contr (A : Type₊) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
definition trunc_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
trunc_index.rec_on n H _
definition trunc_hprop (A : Type₊) (n : trunc_index) [H : is_hprop A]
definition trunc_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
: is_trunc (n.+1) A :=
trunc_leq A -1 (n.+1) star
definition trunc_hset (A : Type₊) (n : trunc_index) [H : is_hset A]
definition trunc_hset (A : Type) (n : trunc_index) [H : is_hset A]
: is_trunc (n.+2) A :=
trunc_leq A 0 (n.+2) star
@ -152,22 +152,22 @@ namespace truncation
definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y :=
@center _ !succ_is_trunc
definition contr_inhabited_hprop {A : Type₊} [H : is_hprop A] (x : A) : is_contr A :=
definition contr_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A :=
is_contr.mk x (λy, !is_hprop.elim)
--Coq has the following as instance, but doesn't look too useful
definition hprop_inhabited_contr {A : Type₊} (H : A → is_contr A) : is_hprop A :=
definition hprop_inhabited_contr {A : Type} (H : A → is_contr A) : is_hprop A :=
@is_trunc_succ A -2
(λx y,
have H2 [visible] : is_contr A, from H x,
!contr_paths_contr)
definition is_hprop.mk {A : Type₊} (H : ∀x y : A, x ≈ y) : is_hprop A :=
definition is_hprop.mk {A : Type} (H : ∀x y : A, x ≈ y) : is_hprop A :=
hprop_inhabited_contr (λ x, is_contr.mk x (H x))
/- hsets -/
definition is_hset.mk (A : Type₊) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
definition is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x ≈ y), p ≈ q) : is_hset A :=
@is_trunc_succ _ _ (λ x y, is_hprop.mk (H x y))
definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x ≈ y) : p ≈ q :=
@ -175,7 +175,7 @@ namespace truncation
/- instances -/
definition contr_basedpaths [instance] {A : Type₊} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
definition contr_basedpaths [instance] {A : Type} (a : A) : is_contr (Σ(x : A), a ≈ x) :=
is_contr.mk (dpair a idp) (λp, sigma.rec_on p (λ b q, path.rec_on q idp))
definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry
@ -189,12 +189,12 @@ namespace truncation
/- truncated universe -/
structure trunctype (n : trunc_index) :=
(trunctype_type : Type₁) (is_trunc_trunctype_type : is_trunc n trunctype_type)
(trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type)
coercion trunctype.trunctype_type
notation n `-Type` := trunctype n
notation `hprop` := -1-Type.
notation `hset` := 0-Type.
notation `hprop` := -1-Type
notation `hset` := 0-Type
definition hprop.mk := @trunctype.mk -1
definition hset.mk := @trunctype.mk 0

270
library/hott/types/sigma.lean Normal file
View file

@ -0,0 +1,270 @@
/-
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 sigma-types (dependent sums)
-/
import ..trunc
open path sigma sigma.ops Equiv IsEquiv
variables {A A' : Type} {B : A → Type} {B' : A' → Type} {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''} {u v w : Σa, B a}
definition eta_sigma : (u.1 ; u.2) ≈ u :=
destruct u (λu1 u2, idp)
definition eta2_sigma (u : Σa b, C a b) : (u.1; u.2.1; u.2.2) ≈ u :=
destruct u (λu1 u2, destruct u2 (λu21 u22, idp))
definition eta3_sigma (u : Σa b c, D a b c) : (u.1; u.2.1; u.2.2.1; u.2.2.2) ≈ u :=
destruct u (λu1 u2, destruct u2 (λu21 u22, destruct u22 (λu221 u222, idp)))
definition path_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
path.rec_on p (λb b' q, path.rec_on q idp) b b' q
/- In Coq they often have to give [u] and [v] explicitly -/
definition path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
destruct u
(λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
p q
-- this is a definition which doesn't use path_sigma', which might have better performance when computing with it, but if there are no problems with the current definition, it can be removed.
-- definition path_sigma_uncurried --{u v : Σa, B a}
-- (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
-- have H : Π{a a' : A} {b : B a} {b' : B a'} (p : a ≈ a') (q : p ▹ b ≈ b'),
-- dpair a b ≈ dpair a' b', from
-- λa a' b b' p, path.rec_on p (λb' q, path.rec_on q idp) b',
-- destruct u
-- (λu1 u2, destruct v (λ v1 v2 pq, destruct pq H))
-- pq
-- this is the curried one you usually want to use in practice
-- definition path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
-- path_sigma_uncurried (dpair p q)
-- A variant of [Forall.dpath_forall] from which uses dependent sums to package things. It cannot go into [Forall] because [Sigma] depends on [Forall]
-- definition dpath_forall'
-- (Q: Σa, B a → Type) {x y : A} (h : x ≈ y)
-- (f : Π p, Q (x ; p)) (g : Π p, Q (y ; p))
-- :
-- (Π p, transport Q (path_Σa, B a (x ; p) (y; _) h 1) (f p) ≈ g (h ≈ p))
-- ≃
-- (Π p, transportD P (fun x => fun p => Q ( x ; p)) h p (f p) ≈ g (transport P h p)).
-- Proof.
-- destruct h.
-- apply equiv_idmap.
-- Defined.
/- Projections of paths from a total space -/
definition pr1_path (p : u ≈ v) : u.1 ≈ v.1 :=
ap dpr1 p
postfix `..1`:10000 := pr1_path
definition pr2_path (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 :=
path.rec_on p idp
--Coq uses the following proof, which only computes if u,v are dpairs AND p is idp
--(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p
postfix `..2`:10000 := pr2_path
definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: dpair (path_sigma p q)..1 (path_sigma p q)..2 ≈ (p; q) :=
begin
generalize q, generalize p,
apply (destruct u), intros (u1, u2),
apply (destruct v), intros (v1, v2, p), generalize v2,
apply (path.rec_on p), intros (v2, q),
apply (path.rec_on q), apply idp
end
definition pr1_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (path_sigma p q)..1 ≈ p :=
(!dpair_path_sigma)..1
definition pr2_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: pr1_path_sigma p q ▹ (path_sigma p q)..2 ≈ q :=
(!dpair_path_sigma)..2
definition eta_path_sigma (p : u ≈ v) : path_sigma (p..1) (p..2) ≈ p :=
begin
apply (path.rec_on p),
apply (destruct u), intros (u1, u2),
apply idp
end
definition transport_pr1_path_sigma {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
: transport (λx, B' x.1) (path_sigma p q) ≈ transport B' p :=
begin
generalize q, generalize p,
apply (destruct u), intros (u1, u2),
apply (destruct v), intros (v1, v2, p), generalize v2,
apply (path.rec_on p), intros (v2, q),
apply (path.rec_on q), apply idp
end
/- the uncurried version of path_sigma. We will prove that this is an equivalence -/
definition path_sigma_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
destruct pq path_sigma
definition dpair_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: dpair (path_sigma_uncurried pq)..1 (path_sigma_uncurried pq)..2 ≈ pq :=
destruct pq dpair_path_sigma
definition pr1_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: (path_sigma_uncurried pq)..1 ≈ pq.1 :=
(!dpair_path_sigma_uncurried)..1
definition pr2_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: (pr1_path_sigma_uncurried pq) ▹ (path_sigma_uncurried pq)..2 ≈ pq.2 :=
(!dpair_path_sigma_uncurried)..2
definition eta_path_sigma_uncurried (p : u ≈ v) : path_sigma_uncurried (dpair p..1 p..2) ≈ p :=
!eta_path_sigma
definition transport_pr1_path_sigma_uncurried {B' : A → Type} (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
: transport (λx, B' x.1) (@path_sigma_uncurried A B u v pq) ≈ transport B' pq.1 :=
destruct pq transport_pr1_path_sigma
definition isequiv_path_sigma [instance] : IsEquiv (@path_sigma_uncurried A B u v) :=
adjointify path_sigma_uncurried
(λp, (p..1; p..2))
eta_path_sigma_uncurried
dpair_path_sigma_uncurried
definition equiv_path_sigma (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
Equiv.mk path_sigma_uncurried _
definition path_sigma_dpair_pp_pp (p1 : a ≈ a' ) (q1 : p1 ▹ b ≈ b' )
(p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
path_sigma_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
≈ path_sigma_dpair p1 q1 ⬝ path_sigma_dpair p2 q2 :=
begin
generalize q2, generalize q1, generalize b'', generalize p2, generalize b',
apply (path.rec_on p1), intros (b', p2),
apply (path.rec_on p2), intros (b'', q1),
apply (path.rec_on q1), intro q2,
apply (path.rec_on q2), apply idp
end
definition path_sigma_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2)
(p2 : v.1 ≈ w.1) (q2 : p2 ▹ v.2 ≈ w.2) :
path_sigma (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
≈ path_sigma p1 q1 ⬝ path_sigma p2 q2 :=
begin
generalize q2, generalize p2, generalize q1, generalize p1,
apply (destruct u), intros (u1, u2),
apply (destruct v), intros (v1, v2),
apply (destruct w), intros,
apply path_sigma_dpair_pp_pp
end
-- definition path_sigma_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
-- path_sigma_dpair p q ≈ path_sigma_dpair p idp ⬝ path_sigma_dpair idp sorry
-- :=
-- sorry
-- begin
-- generalize q,
-- apply (path.rec_on p), intro q,
-- apply (path.rec_on q), apply idp
-- end
/- pr1_path commutes with the groupoid structure. -/
definition pr1_path_1 (u : Σa, B a) : (idpath u)..1 ≈ idpath (u.1) := idp
definition pr1_path_pp (p : u ≈ v) (q : v ≈ w) : (p ⬝ q) ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp
definition pr1_path_V (p : u ≈ v) : p⁻¹ ..1 ≈ (p..1)⁻¹ := !ap_V
/- Applying dpair to one argument is the same as path_sigma_dpair with reflexivity in the first place. -/
definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ path_sigma_dpair idp q :=
path.rec_on q idp
/- Dependent transport is the same as transport along a path_sigma. -/
definition transportD_is_transport (p : a ≈ a') (c : C a b) :
p ▹D c ≈ transport (λu, C (u.1) (u.2)) (path_sigma_dpair p idp) c :=
path.rec_on p idp
definition path_path_sigma_path_sigma {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'}
(r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : path_sigma p1 p2 ≈ path_sigma q1 q2 :=
path.rec_on r
proof (λq2 s, path.rec_on s idp) qed
q2
s
-- begin
-- generalize s, generalize q2,
-- apply (path.rec_on r), intros (q2, s),
-- apply (path.rec_on s), apply idp
-- end
/- A path between paths in a total space is commonly shown component wise. -/
definition path_path_sigma {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
begin
generalize s, generalize r, generalize q,
apply (path.rec_on p),
apply (destruct u), intros (u1, u2, q, r, s),
apply concat, rotate 1,
apply eta_path_sigma,
apply (path_path_sigma_path_sigma r s)
end
/- In Coq they often have to give u and v explicitly when using the following definition -/
definition path_path_sigma_uncurried {p q : u ≈ v}
(rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
destruct rs path_path_sigma
/- Transport -/
/- The concrete description of transport in sigmas (and also pis) is rather trickier than in the other types. In particular, these cannot be described just in terms of transport in simpler types; they require also the dependent transport [transportD].
In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory). A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/
definition transport_sigma (p : a ≈ a') (bc : Σ(b : B a), C a b) : p ▹ bc ≈ (p ▹ bc.1; p ▹D bc.2)
:=
begin
apply (path.rec_on p),
apply (destruct bc), intros (b, c),
apply idp
end
/- The special case when the second variable doesn't depend on the first is simpler. -/
definition transport_sigma' {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b)
: p ▹ bc ≈ (bc.1; p ▹ bc.2) :=
begin
apply (path.rec_on p),
apply (destruct bc), intros (b, c),
apply idp
end
/- Or if the second variable contains a first component that doesn't depend on the first. Need to think about the naming of these. -/
definition transport_sigma_' {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
(bcd : Σ(b : B a) (c : C a), D a b c) : p ▹ bcd ≈ (p ▹ bcd.1; p ▹ bcd.2.1; p ▹D2 bcd.2.2) :=
begin
generalize bcd,
apply (path.rec_on p), intro bcd,
apply (destruct bcd), intros (b, cd),
apply (destruct cd), intros (c, d),
apply idp
end
/- Functorial action -/
variables {f : A → A'} {g : Πa, B a → B' (f a)}
definition functor_sigma (f : A → A') (g : Πa, B a → B' (f a)) (u : Σa, B a) : Σa', B' a' :=
(f u.1; g u.1 u.2)
/- ** Equivalences -/
-- definition isequiv_functor_sigma [instance] [H1 : IsEquiv f] [H2 : Π a, IsEquiv (g a)]
-- : IsEquiv (functor_sigma f g) :=
-- sorry