diff --git a/library/data/sigma/thms.lean b/library/data/sigma/thms.lean index 8745615c3..a29a8f8b8 100644 --- a/library/data/sigma/thms.lean +++ b/library/data/sigma/thms.lean @@ -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} : diff --git a/library/hott/equiv.lean b/library/hott/equiv.lean index 02f4353d6..01400a871 100644 --- a/library/hott/equiv.lean +++ b/library/hott/equiv.lean @@ -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 diff --git a/library/hott/path.lean b/library/hott/path.lean index 34606e4a4..fb43ab968 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -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 diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 19d59958d..32babec81 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -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 diff --git a/library/hott/types/sigma.lean b/library/hott/types/sigma.lean new file mode 100644 index 000000000..43e08c864 --- /dev/null +++ b/library/hott/types/sigma.lean @@ -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