diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean index 65fb6df59..176a2e073 100644 --- a/hott/algebra/binary.hlean +++ b/hott/algebra/binary.hlean @@ -8,8 +8,7 @@ Authors: Leonardo de Moura, Jeremy Avigad General properties of binary operations. -/ -import hott.path -open path +open eq namespace path_binary section @@ -20,26 +19,26 @@ namespace path_binary notation [local] a ⁻¹ := inv a notation [local] 1 := one - definition commutative := ∀a b, a*b ≈ b*a - definition associative := ∀a b c, (a*b)*c ≈ a*(b*c) - definition left_identity := ∀a, 1 * a ≈ a - definition right_identity := ∀a, a * 1 ≈ a - definition left_inverse := ∀a, a⁻¹ * a ≈ 1 - definition right_inverse := ∀a, a * a⁻¹ ≈ 1 - definition left_cancelative := ∀a b c, a * b ≈ a * c → b ≈ c - definition right_cancelative := ∀a b c, a * b ≈ c * b → a ≈ c + definition commutative := ∀a b, a*b = b*a + definition associative := ∀a b c, (a*b)*c = a*(b*c) + definition left_identity := ∀a, 1 * a = a + definition right_identity := ∀a, a * 1 = a + definition left_inverse := ∀a, a⁻¹ * a = 1 + definition right_inverse := ∀a, a * a⁻¹ = 1 + definition left_cancelative := ∀a b c, a * b = a * c → b = c + definition right_cancelative := ∀a b c, a * b = c * b → a = c - definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) ≈ b - definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) ≈ b - definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b ≈ a - definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ ≈ a + definition inv_op_cancel_left := ∀a b, a⁻¹ * (a * b) = b + definition op_inv_cancel_left := ∀a b, a * (a⁻¹ * b) = b + definition inv_op_cancel_right := ∀a b, a * b⁻¹ * b = a + definition op_inv_cancel_right := ∀a b, a * b * b⁻¹ = a variable (op₂ : A → A → A) notation [local] a + b := op₂ a b - definition left_distributive := ∀a b c, a * (b + c) ≈ a * b + a * c - definition right_distributive := ∀a b c, (a + b) * c ≈ a * c + b * c + definition left_distributive := ∀a b c, a * (b + c) = a * b + a * c + definition right_distributive := ∀a b c, (a + b) * c = a * c + b * c end context @@ -48,17 +47,17 @@ namespace path_binary variable H_comm : commutative f variable H_assoc : associative f infixl `*` := f - theorem left_comm : ∀a b c, a*(b*c) ≈ b*(a*c) := + theorem left_comm : ∀a b c, a*(b*c) = b*(a*c) := take a b c, calc - a*(b*c) ≈ (a*b)*c : H_assoc - ... ≈ (b*a)*c : H_comm - ... ≈ b*(a*c) : H_assoc + a*(b*c) = (a*b)*c : H_assoc + ... = (b*a)*c : H_comm + ... = b*(a*c) : H_assoc - theorem right_comm : ∀a b c, (a*b)*c ≈ (a*c)*b := + theorem right_comm : ∀a b c, (a*b)*c = (a*c)*b := take a b c, calc - (a*b)*c ≈ a*(b*c) : H_assoc - ... ≈ a*(c*b) : H_comm - ... ≈ (a*c)*b : H_assoc + (a*b)*c = a*(b*c) : H_assoc + ... = a*(c*b) : H_comm + ... = (a*c)*b : H_assoc end context @@ -66,10 +65,10 @@ namespace path_binary variable {f : A → A → A} variable H_assoc : associative f infixl `*` := f - theorem assoc4helper (a b c d) : (a*b)*(c*d) ≈ a*((b*c)*d) := + theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) := calc - (a*b)*(c*d) ≈ a*(b*(c*d)) : H_assoc - ... ≈ a*((b*c)*d) : H_assoc + (a*b)*(c*d) = a*(b*(c*d)) : H_assoc + ... = a*((b*c)*d) : H_assoc end end path_binary diff --git a/hott/algebra/relation.hlean b/hott/algebra/relation.hlean index ead65fef1..95d476061 100644 --- a/hott/algebra/relation.hlean +++ b/hott/algebra/relation.hlean @@ -94,14 +94,14 @@ namespace is_congruence is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H)) theorem const {T2 : Type} (R2 : T2 → T2 → Type) (H : relation.reflexive R2) - ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : + ⦃T1 : Type⦄ (R1 : T1 → T1 → Type) (c : T2) : is_congruence R1 R2 (λu : T1, c) := is_congruence.mk (λx y H1, H c) end is_congruence theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Type) - [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : + [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Type) (c : T2) : is_congruence R1 R2 (λu : T1, c) := is_congruence.const R2 (is_reflexive.refl R2) R1 c diff --git a/hott/default.hlean b/hott/default.hlean index 4e38ab29c..d6dda5b5c 100644 --- a/hott/default.hlean +++ b/hott/default.hlean @@ -1,10 +1,8 @@ -- Copyright (c) 2014 Jeremy Avigad. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad +-- Author: Jeremy Avigad, Jakob von Raumer -- hott.default -- ============ -- A library for homotopy type theory - -import ..standard .path .equiv .trunc .fibrant \ No newline at end of file diff --git a/hott/equiv_precomp.hlean b/hott/equiv_precomp.hlean index 79133ebd7..81c44c97f 100644 --- a/hott/equiv_precomp.hlean +++ b/hott/equiv_precomp.hlean @@ -2,8 +2,8 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jakob von Raumer -- Ported from Coq HoTT -import hott.equiv hott.axioms.funext -open path function funext +import init.equiv init.axioms.funext +open eq function funext namespace is_equiv context @@ -34,12 +34,12 @@ namespace is_equiv --the domain or the codomain. protected definition isequiv_precompose_eq {A B : Type} (f : A → B) (C D : Type) (Ceq : is_equiv (precomp f C)) (Deq : is_equiv (precomp f D)) (k : C → D) (h : A → C) : - k ∘ (inv (precomp f C)) h ≈ (inv (precomp f D)) (k ∘ h) := + k ∘ (inv (precomp f C)) h = (inv (precomp f D)) (k ∘ h) := let invD := inv (precomp f D) in let invC := inv (precomp f C) in - have eq1 : invD (k ∘ h) ≈ k ∘ (invC h), - from calc invD (k ∘ h) ≈ invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h - ... ≈ k ∘ (invC h) : !sect, + have eq1 : invD (k ∘ h) = k ∘ (invC h), + from calc invD (k ∘ h) = invD (k ∘ (precomp f C (invC h))) : retr (precomp f C) h + ... = k ∘ (invC h) : !sect, eq1⁻¹ definition from_isequiv_precomp {A B : Type} (f : A → B) (Aeq : is_equiv (precomp f A)) @@ -47,14 +47,14 @@ namespace is_equiv let invA := inv (precomp f A) in let invB := inv (precomp f B) in let sect' : f ∘ (invA id) ∼ id := (λx, - calc f (invA id x) ≈ (f ∘ invA id) x : idp - ... ≈ invB (f ∘ id) x : apD10 (!isequiv_precompose_eq) - ... ≈ invB (precomp f B id) x : idp - ... ≈ x : apD10 (sect (precomp f B) id)) + calc f (invA id x) = (f ∘ invA id) x : idp + ... = invB (f ∘ id) x : apD10 (!isequiv_precompose_eq) + ... = invB (precomp f B id) x : idp + ... = x : apD10 (sect (precomp f B) id)) in let retr' : (invA id) ∘ f ∼ id := (λx, - calc invA id (f x) ≈ precomp f A (invA id) x : idp - ... ≈ x : apD10 (retr (precomp f A) id)) in + calc invA id (f x) = precomp f A (invA id) x : idp + ... = x : apD10 (retr (precomp f A) id)) in adjointify f (invA id) sect' retr' end diff --git a/hott/axioms/funext.hlean b/hott/init/axioms/funext.hlean similarity index 83% rename from hott/axioms/funext.hlean rename to hott/init/axioms/funext.hlean index 6f7ae3ccd..110b876ac 100644 --- a/hott/axioms/funext.hlean +++ b/hott/init/axioms/funext.hlean @@ -2,9 +2,9 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad, Jakob von Raumer -- Ported from Coq HoTT - -import hott.path hott.equiv -open path +prelude +import ..path ..equiv +open eq -- Funext -- ------ @@ -23,12 +23,12 @@ namespace funext protected definition ap [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) := rec_on F (λ(H : Π A P f g, _), !H) - definition path_pi {f g : Π x, P x} : f ∼ g → f ≈ g := + definition path_pi {f g : Π x, P x} : f ∼ g → f = g := is_equiv.inv (@apD10 A P f g) omit F definition path_pi2 [F : funext] {A B : Type} {P : A → B → Type} - (f g : Πx y, P x y) : (Πx y, f x y ≈ g x y) → f ≈ g := + (f g : Πx y, P x y) : (Πx y, f x y = g x y) → f = g := λ E, path_pi (λx, path_pi (E x)) end funext diff --git a/hott/init/funext_from_ua.hlean b/hott/init/axioms/funext_from_ua.hlean similarity index 77% rename from hott/init/funext_from_ua.hlean rename to hott/init/axioms/funext_from_ua.hlean index 7838431d5..46083b6a0 100644 --- a/hott/init/funext_from_ua.hlean +++ b/hott/init/axioms/funext_from_ua.hlean @@ -2,10 +2,11 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jakob von Raumer -- Ported from Coq HoTT -import hott.equiv hott.funext_varieties hott.axioms.ua hott.axioms.funext -import data.prod data.sigma data.unit +prelude +import ..equiv ..datatypes +import .funext_varieties .ua .funext -open path function prod sigma truncation equiv is_equiv unit ua_type +open eq function prod sigma truncation equiv is_equiv unit ua_type context universe variables l @@ -14,38 +15,38 @@ context protected theorem ua_isequiv_postcompose {A B : Type.{l+1}} {C : Type} {w : A → B} {H0 : is_equiv w} : is_equiv (@compose C A B w) := let w' := equiv.mk w H0 in - let eqinv : A ≈ B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in + let eqinv : A = B := ((@is_equiv.inv _ _ _ (@ua_type.inst UA A B)) w') in let eq' := equiv_path eqinv in is_equiv.adjointify (@compose C A B w) (@compose C B A (is_equiv.inv w)) (λ (x : C → B), - have eqretr : eq' ≈ w', + have eqretr : eq' = w', from (@retr _ _ (@equiv_path A B) (@ua_type.inst UA A B) w'), - have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹, + have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹, from inv_eq eq' w' eqretr, - have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x, + have eqfin : (to_fun eq') ∘ ((to_fun eq')⁻¹ ∘ x) = x, from (λ p, - (@path.rec_on Type.{l+1} A + (@eq.rec_on Type.{l+1} A (λ B' p', Π (x' : C → B'), (to_fun (equiv_path p')) - ∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') ≈ x') + ∘ ((to_fun (equiv_path p'))⁻¹ ∘ x') = x') B p (λ x', idp)) ) eqinv x, - have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) ≈ x, + have eqfin' : (to_fun w') ∘ ((to_fun eq')⁻¹ ∘ x) = x, from eqretr ▹ eqfin, - have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) ≈ x, + have eqfin'' : (to_fun w') ∘ ((to_fun w')⁻¹ ∘ x) = x, from invs_eq ▹ eqfin', eqfin'' ) (λ (x : C → A), - have eqretr : eq' ≈ w', + have eqretr : eq' = w', from (@retr _ _ (@equiv_path A B) ua_type.inst w'), - have invs_eq : (to_fun eq')⁻¹ ≈ (to_fun w')⁻¹, + have invs_eq : (to_fun eq')⁻¹ = (to_fun w')⁻¹, from inv_eq eq' w' eqretr, - have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) ≈ x, - from (λ p, path.rec_on p idp) eqinv, - have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x, + have eqfin : (to_fun eq')⁻¹ ∘ ((to_fun eq') ∘ x) = x, + from (λ p, eq.rec_on p idp) eqinv, + have eqfin' : (to_fun eq')⁻¹ ∘ ((to_fun w') ∘ x) = x, from eqretr ▹ eqfin, - have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) ≈ x, + have eqfin'' : (to_fun w')⁻¹ ∘ ((to_fun w') ∘ x) = x, from invs_eq ▹ eqfin', eqfin'' ) @@ -53,7 +54,7 @@ context -- 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 + := Σ xy : B × B, pr₁ xy = pr₂ xy protected definition isequiv_src_compose {A B : Type} : @is_equiv (A → diagonal B) @@ -64,7 +65,7 @@ context (λ 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)))) + (λ b c p, eq.rec_on p idp)))) protected definition isequiv_tgt_compose {A B : Type} : @is_equiv (A → diagonal B) @@ -75,10 +76,10 @@ context (λ 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)))) + (λ b c p, eq.rec_on p idp)))) theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}} - : Π {f g : A → B}, f ∼ g → f ≈ g := + : Π {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 @@ -88,13 +89,13 @@ context have equiv2 [visible] : Π x y, is_equiv (ap precomp1), from is_equiv.ap_closed precomp1, have H' : Π (x y : A → diagonal B), - pr₁ ∘ dpr1 ∘ x ≈ pr₁ ∘ dpr1 ∘ y → x ≈ y, + pr₁ ∘ dpr1 ∘ x = pr₁ ∘ dpr1 ∘ y → x = y, from (λ x y, is_equiv.inv (ap precomp1)), - have eq2 : pr₁ ∘ dpr1 ∘ d ≈ pr₁ ∘ dpr1 ∘ e, + have eq2 : pr₁ ∘ dpr1 ∘ d = pr₁ ∘ dpr1 ∘ e, from idp, - have eq0 : d ≈ e, + have eq0 : d = e, from H' d e eq2, - have eq1 : (pr₂ ∘ dpr1) ∘ d ≈ (pr₂ ∘ dpr1) ∘ e, + have eq1 : (pr₂ ∘ dpr1) ∘ d = (pr₂ ∘ dpr1) ∘ e, from ap _ eq0, eq1 ) @@ -109,10 +110,10 @@ theorem weak_funext_from_ua [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_f let U := (λ (x : A), unit) in have pequiv : Π (x : A), P x ≃ U x, from (λ x, @equiv_contr_unit(P x) (allcontr x)), - have psim : Π (x : A), P x ≈ U x, + have psim : Π (x : A), P x = U x, from (λ x, @is_equiv.inv _ _ equiv_path ua_type.inst (pequiv x)), - have p : P ≈ U, + have p : P = U, from @nondep_funext_from_ua _ A Type P U psim, have tU' : is_contr (A → unit), from is_contr.mk (λ x, ⋆) @@ -121,7 +122,7 @@ theorem weak_funext_from_ua [ua3 : ua_type.{k+1}] [ua4 : ua_type.{k+2}] : weak_f have tU : is_contr (Π x, U x), from tU', have tlast : is_contr (Πx, P x), - from path.transport _ (p⁻¹) tU, + from eq.transport _ (p⁻¹) tU, tlast ) diff --git a/hott/init/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean similarity index 78% rename from hott/init/funext_varieties.hlean rename to hott/init/axioms/funext_varieties.hlean index a0fadb896..a100693f9 100644 --- a/hott/init/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -2,9 +2,9 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Jakob von Raumer -- Ported from Coq HoTT -import hott.path hott.trunc hott.equiv hott.axioms.funext +import ..path ..trunc ..equiv .funext -open path truncation sigma function +open eq truncation sigma function /- 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 @@ -17,7 +17,7 @@ open path truncation sigma function -- Naive funext is the simple assertion that pointwise equal functions are equal. -- TODO think about universe levels definition naive_funext := - Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f ≈ g + Π {A : Type} {P : A → Type} (f g : Πx, P x), (f ∼ g) → f = g -- Weak funext says that a product of contractible types is contractible. definition weak_funext.{l k} := @@ -39,7 +39,7 @@ definition weak_funext_from_naive_funext : naive_funext → weak_funext := is_contr.mk c (λ f, have eq' : (λx, center (P x)) ∼ f, from (λx, contr (f x)), - have eq : (λx, center (P x)) ≈ f, + have eq : (λx, center (P x)) = f, from nf A P (λx, center (P x)) f eq', eq ) @@ -60,19 +60,19 @@ context is_contr.mk (dpair f idhtpy) (λ dp, sigma.rec_on dp (λ (g : Π x, B x) (h : f ∼ g), - let r := λ (k : Π x, Σ y, f x ≈ y), + let r := λ (k : Π x, Σ y, f x = y), @dpair _ (λg, f ∼ g) (λx, dpr1 (k x)) (λx, dpr2 (k x)) in - let s := λ g h x, @dpair _ (λy, f x ≈ y) (g x) (h x) in - have t1 : Πx, is_contr (Σ y, f x ≈ y), + let s := λ g h x, @dpair _ (λy, f x = y) (g x) (h x) in + have t1 : Πx, is_contr (Σ y, f x = y), from (λx, !contr_basedpaths), - have t2 : is_contr (Πx, Σ y, f x ≈ y), + have t2 : is_contr (Πx, Σ y, f x = y), from !wf, - have t3 : (λ x, @dpair _ (λ y, f x ≈ y) (f x) idp) ≈ s g h, - from @path_contr (Π x, Σ y, f x ≈ y) t2 _ _, - have t4 : r (λ x, dpair (f x) idp) ≈ r (s g h), + have t3 : (λ x, @dpair _ (λ y, f x = y) (f x) idp) = s g h, + from @path_contr (Π x, Σ y, f x = y) t2 _ _, + have t4 : r (λ x, dpair (f x) idp) = r (s g h), from ap r t3, - have endt : dpair f idhtpy ≈ dpair g h, + have endt : dpair f idhtpy = dpair g h, from t4, endt ) @@ -84,7 +84,7 @@ context @transport _ (λ gh, Q (dpr1 gh) (dpr2 gh)) (dpair f idhtpy) (dpair g h) (@path_contr _ contr_basedhtpy _ _) d - definition htpy_ind_beta : htpy_ind f idhtpy ≈ d := + definition htpy_ind_beta : htpy_ind f idhtpy = d := (@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp end @@ -94,16 +94,16 @@ universe variables l k theorem funext_from_weak_funext (wf : weak_funext.{l+1 k+1}) : funext.{l+1 k+1} := funext.mk (λ A B f g, - let eq_to_f := (λ g' x, f ≈ g') in + let eq_to_f := (λ g' x, f = g') in let sim2path := htpy_ind _ f eq_to_f idp in - have t1 : sim2path f (idhtpy f) ≈ idp, + have t1 : sim2path f (idhtpy f) = idp, proof htpy_ind_beta _ f eq_to_f idp qed, - have t2 : apD10 (sim2path f (idhtpy f)) ≈ (idhtpy f), + have t2 : apD10 (sim2path f (idhtpy f)) = (idhtpy f), proof ap apD10 t1 qed, have sect : apD10 ∘ (sim2path g) ∼ id, - proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) ≈ x) t2) g qed, + proof (htpy_ind _ f (λ g' x, apD10 (sim2path g' x) = x) t2) g qed, have retr : (sim2path g) ∘ apD10 ∼ id, - from (λ h, path.rec_on h (htpy_ind_beta _ f _ idp)), + from (λ h, eq.rec_on h (htpy_ind_beta _ f _ idp)), is_equiv.adjointify apD10 (sim2path g) sect retr) definition funext_from_naive_funext : naive_funext -> funext := diff --git a/hott/init/ua.hlean b/hott/init/axioms/ua.hlean similarity index 84% rename from hott/init/ua.hlean rename to hott/init/axioms/ua.hlean index 007850d3f..bdcda8d63 100644 --- a/hott/init/ua.hlean +++ b/hott/init/axioms/ua.hlean @@ -2,18 +2,19 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jakob von Raumer -- Ported from Coq HoTT -import hott.path hott.equiv -open path equiv +prelude +import ..path ..equiv +open eq equiv --Ensure that the types compared are in the same universe section universe variable l variables {A B : Type.{l}} - definition isequiv_path (H : A ≈ B) := + definition isequiv_path (H : A = B) := (@is_equiv.transport Type (λX, X) A B H) - definition equiv_path (H : A ≈ B) : A ≃ B := + definition equiv_path (H : A = B) : A ≃ B := equiv.mk _ (isequiv_path H) end @@ -32,7 +33,7 @@ namespace ua_type rec_on F (λ H, H A B) -- This is the version of univalence axiom we will probably use most often - definition ua : A ≃ B → A ≈ B := + definition ua : A ≃ B → A = B := @is_equiv.inv _ _ (@equiv_path A B) inst end @@ -45,7 +46,7 @@ namespace Equiv protected definition subst [UA : ua_type] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B) : P A → P B := - path.transport P (ua_type.ua H) + eq.transport P (ua_type.ua H) -- We can use this for calculation evironments calc_subst subst diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean index aecd208ac..cbff1f7ff 100644 --- a/hott/init/datatypes.hlean +++ b/hott/init/datatypes.hlean @@ -2,7 +2,7 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Jakob von Raumer Basic datatypes -/ @@ -17,7 +17,13 @@ notation `Type₃` := Type.{3} inductive unit.{l} : Type.{l} := star : unit -inductive empty : Type +namespace unit + + notation `⋆` := star + +end unit + +inductive empty.{l} : Type.{l} inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} := refl : eq a a diff --git a/hott/init/default.hlean b/hott/init/default.hlean index 1cbeb2a5f..c865a3ba2 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -6,5 +6,6 @@ Authors: Leonardo de Moura -/ prelude import init.datatypes init.reserved_notation init.tactic init.logic -import init.bool init.num init.priority init.relation init.wf init.prod -import init.sigma +import init.bool init.num init.priority init.relation init.wf +import init.types.sigma init.types.prod +import init.trunc init.path init.equiv diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 727a49ccf..598a7bfcb 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -2,8 +2,9 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jeremy Avigad, Jakob von Raumer -- Ported from Coq HoTT -import .path -open path function +prelude +import .path .function +open eq function -- Equivalences -- ------------ @@ -14,7 +15,7 @@ structure is_equiv [class] {A B : Type} (f : A → B) := (inv : B → A) (retr : (f ∘ inv) ∼ id) (sect : (inv ∘ f) ∼ id) - (adj : Πx, retr (f x) ≈ ap f (sect x)) + (adj : Πx, retr (f x) = ap f (sect x)) -- A more bundled version of equivalence to calculate with @@ -47,8 +48,8 @@ namespace is_equiv ) -- Any function equal to an equivalence is an equivlance as well. - definition path_closed [Hf : is_equiv f] (Heq : f ≈ f') : (is_equiv f') := - path.rec_on Heq Hf + definition path_closed [Hf : is_equiv f] (Heq : f = f') : (is_equiv f') := + eq.rec_on Heq Hf -- Any function pointwise equal to an equivalence is an equivalence as well. definition homotopy_closed [Hf : is_equiv f] (Hty : f ∼ f') : (is_equiv f') := @@ -60,26 +61,26 @@ namespace is_equiv let secta := sect f a in let retrfa := retr f (f a) in let retrf'a := retr f (f' a) in - have eq1 : _ ≈ _, + have eq1 : _ = _, from calc ap f secta ⬝ ff'a - ≈ retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _) - ... ≈ ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p - ... ≈ ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f, - have eq2 : _ ≈ _, + = retrfa ⬝ ff'a : ap _ (@adj _ _ f _ _) + ... = ap (f ∘ invf) ff'a ⬝ retrf'a : concat_A1p + ... = ap f (ap invf ff'a) ⬝ retrf'a : ap_compose invf f, + have eq2 : _ = _, from calc retrf'a - ≈ (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹) - ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a - ... ≈ ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap - ... ≈ (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p - ... ≈ (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V - ... ≈ (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap - ... ≈ (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V - ... ≈ Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p, - have eq3 : _ ≈ _, + = (ap f (ap invf ff'a))⁻¹ ⬝ (ap f secta ⬝ ff'a) : moveL_Vp _ _ _ (eq1⁻¹) + ... = ap f (ap invf ff'a)⁻¹ ⬝ (ap f secta ⬝ Hty a) : ap_V invf ff'a + ... = ap f (ap invf ff'a)⁻¹ ⬝ (Hty (invf (f a)) ⬝ ap f' secta) : concat_Ap + ... = (ap f (ap invf ff'a)⁻¹ ⬝ Hty (invf (f a))) ⬝ ap f' secta : concat_pp_p + ... = (ap f ((ap invf ff'a)⁻¹) ⬝ Hty (invf (f a))) ⬝ ap f' secta : ap_V + ... = (Hty (invf (f' a)) ⬝ ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : concat_Ap + ... = (Hty (invf (f' a)) ⬝ (ap f' (ap invf ff'a))⁻¹) ⬝ ap f' secta : ap_V + ... = Hty (invf (f' a)) ⬝ ((ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta) : concat_pp_p, + have eq3 : _ = _, from calc (Hty (invf (f' a)))⁻¹ ⬝ retrf'a - ≈ (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2 - ... ≈ (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V - ... ≈ ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp, + = (ap f' (ap invf ff'a))⁻¹ ⬝ ap f' secta : moveR_Vp _ _ _ eq2 + ... = (ap f' ((ap invf ff'a)⁻¹)) ⬝ ap f' secta : ap_V + ... = ap f' ((ap invf ff'a)⁻¹ ⬝ secta) : ap_pp, eq3) in is_equiv.mk (inv f) sect' retr' adj' end is_equiv @@ -92,34 +93,34 @@ namespace is_equiv definition adjointify_sect' : g ∘ f ∼ id := (λx, ap g (ap f (inverse (sec x))) ⬝ ap g (ret (f x)) ⬝ sec x) - definition adjointify_adj' : Π (x : A), ret (f x) ≈ ap f (adjointify_sect' x) := + definition adjointify_adj' : Π (x : A), ret (f x) = ap f (adjointify_sect' x) := (λ (a : A), let fgretrfa := ap f (ap g (ret (f a))) in let fgfinvsect := ap f (ap g (ap f ((sec a)⁻¹))) in let fgfa := f (g (f a)) in let retrfa := ret (f a) in - have eq1 : ap f (sec a) ≈ _, + have eq1 : ap f (sec a) = _, from calc ap f (sec a) - ≈ idp ⬝ ap f (sec a) : !concat_1p⁻¹ - ... ≈ (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV - ... ≈ ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹} - ... ≈ ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _} - ... ≈ (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p, - have eq2 : ap f (sec a) ⬝ idp ≈ (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)), + = idp ⬝ ap f (sec a) : !concat_1p⁻¹ + ... = (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV + ... = ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹} + ... = ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _} + ... = (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p, + have eq2 : ap f (sec a) ⬝ idp = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)), from !concat_p1 ⬝ eq1, - have eq3 : idp ≈ _, + have eq3 : idp = _, from calc idp - ≈ (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2 - ... ≈ (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp - ... ≈ (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹} - ... ≈ ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp - ... ≈ ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹} - ... ≈ ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _} - ... ≈ (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹} - ... ≈ retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹} - ... ≈ retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹ - ... ≈ retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹}, - have eq4 : ret (f a) ≈ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a), + = (ap f (sec a))⁻¹ ⬝ ((ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a))) : moveL_Vp _ _ _ eq2 + ... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_p_pp + ... = (ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : {!ap_V⁻¹} + ... = ((ap f ((sec a)⁻¹) ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : !concat_p_pp + ... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f ((sec a)⁻¹))) ⬝ fgretrfa) ⬝ ap f (sec a) : {!concat_pA1⁻¹} + ... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _} + ... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : {!concat_p_pp⁻¹} + ... = retrfa⁻¹ ⬝ ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : {!ap_pp⁻¹} + ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : !concat_p_pp⁻¹ + ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a) : {!ap_pp⁻¹}, + have eq4 : ret (f a) = ap f ((ap g (ap f ((sec a)⁻¹)) ⬝ ap g (ret (f a))) ⬝ sec a), from moveR_M1 _ _ eq3, eq4) @@ -153,16 +154,16 @@ namespace is_equiv @homotopy_closed _ _ _ _ (compose (f ∘ g) (f⁻¹)) (λa, sect f (g a)) --Rewrite rules - definition moveR_M {x : A} {y : B} (p : x ≈ (inv f) y) : (f x ≈ y) := + definition moveR_M {x : A} {y : B} (p : x = (inv f) y) : (f x = y) := (ap f p) ⬝ (@retr _ _ f _ y) - definition moveL_M {x : A} {y : B} (p : (inv f) y ≈ x) : (y ≈ f x) := + definition moveL_M {x : A} {y : B} (p : (inv f) y = x) : (y = f x) := (moveR_M f (p⁻¹))⁻¹ - definition moveR_V {x : B} {y : A} (p : x ≈ f y) : (inv f) x ≈ y := + definition moveR_V {x : B} {y : A} (p : x = f y) : (inv f) x = y := ap (f⁻¹) p ⬝ sect f y - definition moveL_V {x : B} {y : A} (p : f y ≈ x) : y ≈ (inv f) x := + definition moveL_V {x : B} {y : A} (p : f y = x) : y = (inv f) x := (moveR_V f (p⁻¹))⁻¹ definition ap_closed [instance] (x y : A) : is_equiv (ap f) := @@ -191,20 +192,20 @@ namespace is_equiv definition equiv_rect (P : B -> Type) : (Πx, P (f x)) → (Πy, P y) := - (λg y, path.transport _ (retr f y) (g (f⁻¹ y))) + (λg y, eq.transport _ (retr f y) (g (f⁻¹ y))) definition equiv_rect_comp (P : B → Type) - (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) ≈ df x := + (df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x := calc equiv_rect f P df (f x) - ≈ transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp - ... ≈ transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f - ... ≈ transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose - ... ≈ df x : apD df (sect f x) + = transport P (retr f (f x)) (df (f⁻¹ (f x))) : idp + ... = transport P (ap f (sect f x)) (df (f⁻¹ (f x))) : adj f + ... = transport (P ∘ f) (sect f x) (df (f⁻¹ (f x))) : transport_compose + ... = df x : apD df (sect f x) end --Transporting is an equivalence - protected definition transport [instance] (P : A → Type) {x y : A} (p : x ≈ y) : (is_equiv (transport P p)) := + protected definition transport [instance] (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := is_equiv.mk (transport P (p⁻¹)) (transport_pV P p) (transport_Vp P p) (transport_pVp P p) end is_equiv @@ -227,7 +228,7 @@ namespace equiv equiv.mk ((to_fun eqg) ∘ f) (is_equiv.compose f (to_fun eqg)) - theorem path_closed (f' : A → B) (Heq : to_fun eqf ≈ f') : A ≃ B := + theorem path_closed (f' : A → B) (Heq : to_fun eqf = f') : A ≃ B := equiv.mk f' (is_equiv.path_closed f Heq) theorem symm : B ≃ A := @@ -239,7 +240,7 @@ namespace equiv theorem cancel_L (g : C → A) [Hgf : is_equiv (f ∘ g)] : C ≃ A := equiv.mk g (is_equiv.cancel_L f _) - protected 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) (is_equiv.transport P p) end @@ -251,9 +252,9 @@ namespace equiv private definition Hg [instance] : is_equiv (to_fun eqg) := to_is_equiv eqg --We need this theorem for the funext_from_ua proof - theorem inv_eq (p : eqf ≈ eqg) - : is_equiv.inv (to_fun eqf) ≈ is_equiv.inv (to_fun eqg) := - path.rec_on p idp + theorem inv_eq (p : eqf = eqg) + : is_equiv.inv (to_fun eqf) = is_equiv.inv (to_fun eqg) := + eq.rec_on p idp end diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 086f1ea3b..9aee35576 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -1,47 +1,44 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad +-- Author: Jeremy Avigad, Jakob von Raumer -- Ported from Coq HoTT -- -- TODO: things to test: -- o To what extent can we use opaque definitions outside the file? -- o Try doing these proofs with tactics. -- o Try using the simplifier on some of these proofs. +prelude +import .function .datatypes .relation .tactic -import algebra.function +open function eq -open function +-- Path equality +-- ---- -------- --- Path --- ---- - -inductive path.{l} {A : Type.{l}} (a : A) : A → Type.{l} := -idpath : path a a - -namespace path +namespace eq variables {A B C : Type} {P : A → Type} {x y z t : A} - notation a ≈ b := path a b - notation x ≈ y `:>`:50 A:49 := @path A x y - definition idp {a : A} := idpath a + --notation a = b := eq a b + notation x = y `:>`:50 A:49 := @eq A x y + definition idp {a : A} := refl a -- unbased path induction - definition rec' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} - (H : Π (a : A), P a a idp) {a b : A} (p : a ≈ b) : P a b p := - path.rec (H a) p + definition rec' [reducible] {P : Π (a b : A), (a = b) -> Type} + (H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p := + eq.rec (H a) p - definition rec_on' [reducible] {P : Π (a b : A), (a ≈ b) -> Type} {a b : A} (p : a ≈ b) + definition rec_on' [reducible] {P : Π (a b : A), (a = b) -> Type} {a b : A} (p : a = b) (H : Π (a : A), P a a idp) : P a b p := - path.rec (H a) p + eq.rec (H a) p -- Concatenation and inverse -- ------------------------- - definition concat (p : x ≈ y) (q : y ≈ z) : x ≈ z := - path.rec (λu, u) q p + definition concat (p : x = y) (q : y = z) : x = z := + eq.rec (λu, u) q p - definition inverse (p : x ≈ y) : y ≈ x := - path.rec (idpath x) p + definition inverse (p : x = y) : y = x := + eq.rec (refl x) p notation p₁ ⬝ p₂ := concat p₁ p₂ notation p ⁻¹ := inverse p @@ -50,159 +47,159 @@ namespace path -- ------------------------------------ -- The identity path is a right unit. - definition concat_p1 (p : x ≈ y) : p ⬝ idp ≈ p := + definition concat_p1 (p : x = y) : p ⬝ idp = p := rec_on p idp -- The identity path is a right unit. - definition concat_1p (p : x ≈ y) : idp ⬝ p ≈ p := + definition concat_1p (p : x = y) : idp ⬝ p = p := rec_on p idp -- Concatenation is associative. - definition concat_p_pp (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : - p ⬝ (q ⬝ r) ≈ (p ⬝ q) ⬝ r := + definition concat_p_pp (p : x = y) (q : y = z) (r : z = t) : + p ⬝ (q ⬝ r) = (p ⬝ q) ⬝ r := rec_on r (rec_on q idp) - definition concat_pp_p (p : x ≈ y) (q : y ≈ z) (r : z ≈ t) : - (p ⬝ q) ⬝ r ≈ p ⬝ (q ⬝ r) := + definition concat_pp_p (p : x = y) (q : y = z) (r : z = t) : + (p ⬝ q) ⬝ r = p ⬝ (q ⬝ r) := rec_on r (rec_on q idp) -- The left inverse law. - definition concat_pV (p : x ≈ y) : p ⬝ p⁻¹ ≈ idp := + definition concat_pV (p : x = y) : p ⬝ p⁻¹ = idp := rec_on p idp -- The right inverse law. - definition concat_Vp (p : x ≈ y) : p⁻¹ ⬝ p ≈ idp := + definition concat_Vp (p : x = y) : p⁻¹ ⬝ p = idp := rec_on p idp -- Several auxiliary theorems about canceling inverses across associativity. These are somewhat -- redundant, following from earlier theorems. - definition concat_V_pp (p : x ≈ y) (q : y ≈ z) : p⁻¹ ⬝ (p ⬝ q) ≈ q := + definition concat_V_pp (p : x = y) (q : y = z) : p⁻¹ ⬝ (p ⬝ q) = q := rec_on q (rec_on p idp) - definition concat_p_Vp (p : x ≈ y) (q : x ≈ z) : p ⬝ (p⁻¹ ⬝ q) ≈ q := + definition concat_p_Vp (p : x = y) (q : x = z) : p ⬝ (p⁻¹ ⬝ q) = q := rec_on q (rec_on p idp) - definition concat_pp_V (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q⁻¹ ≈ p := + definition concat_pp_V (p : x = y) (q : y = z) : (p ⬝ q) ⬝ q⁻¹ = p := rec_on q (rec_on p idp) - definition concat_pV_p (p : x ≈ z) (q : y ≈ z) : (p ⬝ q⁻¹) ⬝ q ≈ p := + definition concat_pV_p (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p := rec_on q (take p, rec_on p idp) p -- Inverse distributes over concatenation - definition inv_pp (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p⁻¹ := + definition inv_pp (p : x = y) (q : y = z) : (p ⬝ q)⁻¹ = q⁻¹ ⬝ p⁻¹ := rec_on q (rec_on p idp) - definition inv_Vp (p : y ≈ x) (q : y ≈ z) : (p⁻¹ ⬝ q)⁻¹ ≈ q⁻¹ ⬝ p := + definition inv_Vp (p : y = x) (q : y = z) : (p⁻¹ ⬝ q)⁻¹ = q⁻¹ ⬝ p := rec_on q (rec_on p idp) -- universe metavariables - definition inv_pV (p : x ≈ y) (q : z ≈ y) : (p ⬝ q⁻¹)⁻¹ ≈ q ⬝ p⁻¹ := + definition inv_pV (p : x = y) (q : z = y) : (p ⬝ q⁻¹)⁻¹ = q ⬝ p⁻¹ := rec_on p (take q, rec_on q idp) q - definition inv_VV (p : y ≈ x) (q : z ≈ y) : (p⁻¹ ⬝ q⁻¹)⁻¹ ≈ q ⬝ p := + definition inv_VV (p : y = x) (q : z = y) : (p⁻¹ ⬝ q⁻¹)⁻¹ = q ⬝ p := rec_on p (rec_on q idp) -- Inverse is an involution. - definition inv_V (p : x ≈ y) : p⁻¹⁻¹ ≈ p := + definition inv_V (p : x = y) : p⁻¹⁻¹ = p := rec_on p idp -- Theorems for moving things around in equations -- ---------------------------------------------- - definition moveR_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - p ≈ (r⁻¹ ⬝ q) → (r ⬝ p) ≈ q := + definition moveR_Mp (p : x = z) (q : y = z) (r : y = x) : + p = (r⁻¹ ⬝ q) → (r ⬝ p) = q := rec_on r (take p h, concat_1p _ ⬝ h ⬝ concat_1p _) p - definition moveR_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - r ≈ q ⬝ p⁻¹ → r ⬝ p ≈ q := + definition moveR_pM (p : x = z) (q : y = z) (r : y = x) : + r = q ⬝ p⁻¹ → r ⬝ p = q := rec_on p (take q h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q - definition moveR_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : - p ≈ r ⬝ q → r⁻¹ ⬝ p ≈ q := + definition moveR_Vp (p : x = z) (q : y = z) (r : x = y) : + p = r ⬝ q → r⁻¹ ⬝ p = q := rec_on r (take q h, concat_1p _ ⬝ h ⬝ concat_1p _) q - definition moveR_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : - r ≈ q ⬝ p → r ⬝ p⁻¹ ≈ q := + definition moveR_pV (p : z = x) (q : y = z) (r : y = x) : + r = q ⬝ p → r ⬝ p⁻¹ = q := rec_on p (take r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) r - definition moveL_Mp (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - r⁻¹ ⬝ q ≈ p → q ≈ r ⬝ p := + definition moveL_Mp (p : x = z) (q : y = z) (r : y = x) : + r⁻¹ ⬝ q = p → q = r ⬝ p := rec_on r (take p h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) p - definition moveL_pM (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) : - q ⬝ p⁻¹ ≈ r → q ≈ r ⬝ p := + definition moveL_pM (p : x = z) (q : y = z) (r : y = x) : + q ⬝ p⁻¹ = r → q = r ⬝ p := rec_on p (take q h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) q - definition moveL_Vp (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) : - r ⬝ q ≈ p → q ≈ r⁻¹ ⬝ p := + definition moveL_Vp (p : x = z) (q : y = z) (r : x = y) : + r ⬝ q = p → q = r⁻¹ ⬝ p := rec_on r (take q h, (concat_1p _)⁻¹ ⬝ h ⬝ (concat_1p _)⁻¹) q - definition moveL_pV (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) : - q ⬝ p ≈ r → q ≈ r ⬝ p⁻¹ := + definition moveL_pV (p : z = x) (q : y = z) (r : y = x) : + q ⬝ p = r → q = r ⬝ p⁻¹ := rec_on p (take r h, (concat_p1 _)⁻¹ ⬝ h ⬝ (concat_p1 _)⁻¹) r - definition moveL_1M (p q : x ≈ y) : - p ⬝ q⁻¹ ≈ idp → p ≈ q := + definition moveL_1M (p q : x = y) : + p ⬝ q⁻¹ = idp → p = q := rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p - definition moveL_M1 (p q : x ≈ y) : - q⁻¹ ⬝ p ≈ idp → p ≈ q := + definition moveL_M1 (p q : x = y) : + q⁻¹ ⬝ p = idp → p = q := rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p - definition moveL_1V (p : x ≈ y) (q : y ≈ x) : - p ⬝ q ≈ idp → p ≈ q⁻¹ := + definition moveL_1V (p : x = y) (q : y = x) : + p ⬝ q = idp → p = q⁻¹ := rec_on q (take p h, (concat_p1 _)⁻¹ ⬝ h) p - definition moveL_V1 (p : x ≈ y) (q : y ≈ x) : - q ⬝ p ≈ idp → p ≈ q⁻¹ := + definition moveL_V1 (p : x = y) (q : y = x) : + q ⬝ p = idp → p = q⁻¹ := rec_on q (take p h, (concat_1p _)⁻¹ ⬝ h) p - definition moveR_M1 (p q : x ≈ y) : - idp ≈ p⁻¹ ⬝ q → p ≈ q := + definition moveR_M1 (p q : x = y) : + idp = p⁻¹ ⬝ q → p = q := rec_on p (take q h, h ⬝ (concat_1p _)) q - definition moveR_1M (p q : x ≈ y) : - idp ≈ q ⬝ p⁻¹ → p ≈ q := + definition moveR_1M (p q : x = y) : + idp = q ⬝ p⁻¹ → p = q := rec_on p (take q h, h ⬝ (concat_p1 _)) q - definition moveR_1V (p : x ≈ y) (q : y ≈ x) : - idp ≈ q ⬝ p → p⁻¹ ≈ q := + definition moveR_1V (p : x = y) (q : y = x) : + idp = q ⬝ p → p⁻¹ = q := rec_on p (take q h, h ⬝ (concat_p1 _)) q - definition moveR_V1 (p : x ≈ y) (q : y ≈ x) : - idp ≈ p ⬝ q → p⁻¹ ≈ q := + definition moveR_V1 (p : x = y) (q : y = x) : + idp = p ⬝ q → p⁻¹ = q := rec_on p (take q h, h ⬝ (concat_1p _)) q -- Transport -- --------- - definition transport [reducible] (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y := - path.rec_on p u + definition transport [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P x) : P y := + eq.rec_on p u -- This idiom makes the operation right associative. notation p `▹`:65 x:64 := transport _ p x - definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x ≈ y) : f x ≈ f y := - path.rec_on p idp + definition ap ⦃A B : Type⦄ (f : A → B) {x y:A} (p : x = y) : f x = f y := + eq.rec_on p idp definition ap01 := ap definition homotopy [reducible] (f g : Πx, P x) : Type := - Πx : A, f x ≈ g x + Πx : A, f x = g x notation f ∼ g := homotopy f g - definition apD10 {f g : Πx, P x} (H : f ≈ g) : f ∼ g := - λx, path.rec_on H idp + definition apD10 {f g : Πx, P x} (H : f = g) : f ∼ g := + λx, eq.rec_on H idp - definition ap10 {f g : A → B} (H : f ≈ g) : f ∼ g := apD10 H + definition ap10 {f g : A → B} (H : f = g) : f ∼ g := apD10 H - definition ap11 {f g : A → B} (H : f ≈ g) {x y : A} (p : x ≈ y) : f x ≈ g y := + definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y := rec_on H (rec_on p idp) - definition apD (f : Πa:A, P a) {x y : A} (p : x ≈ y) : p ▹ (f x) ≈ f y := + definition apD (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ (f x) = f y := rec_on p idp @@ -211,26 +208,26 @@ namespace path calc_subst transport calc_trans concat - calc_refl idpath + calc_refl refl calc_symm inverse -- More theorems for moving things around in equations -- --------------------------------------------------- - definition moveR_transport_p (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : - u ≈ p⁻¹ ▹ v → p ▹ u ≈ v := + definition moveR_transport_p (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) : + u = p⁻¹ ▹ v → p ▹ u = v := rec_on p (take v, id) v - definition moveR_transport_V (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : - u ≈ p ▹ v → p⁻¹ ▹ u ≈ v := + definition moveR_transport_V (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) : + u = p ▹ v → p⁻¹ ▹ u = v := rec_on p (take u, id) u - definition moveL_transport_V (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) : - p ▹ u ≈ v → u ≈ p⁻¹ ▹ v := + definition moveL_transport_V (P : A → Type) {x y : A} (p : x = y) (u : P x) (v : P y) : + p ▹ u = v → u = p⁻¹ ▹ v := rec_on p (take v, id) v - definition moveL_transport_p (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) : - p⁻¹ ▹ u ≈ v → u ≈ p ▹ v := + definition moveL_transport_p (P : A → Type) {x y : A} (p : y = x) (u : P x) (v : P y) : + p⁻¹ ▹ u = v → u = p ▹ v := rec_on p (take u, id) u -- Functoriality of functions @@ -240,115 +237,115 @@ namespace path -- functorial. -- Functions take identity paths to identity paths - definition ap_1 (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp + definition ap_1 (x : A) (f : A → B) : (ap f idp) = idp :> (f x = f x) := idp - definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp ≈ idp :> (f x ≈ f x) := idp + definition apD_1 (x : A) (f : Π x : A, P x) : apD f idp = idp :> (f x = f x) := idp -- Functions commute with concatenation. - definition ap_pp (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) : - ap f (p ⬝ q) ≈ (ap f p) ⬝ (ap f q) := + definition ap_pp (f : A → B) {x y z : A} (p : x = y) (q : y = z) : + ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) := rec_on q (rec_on p idp) - definition ap_p_pp (f : A → B) {w x y z : A} (r : f w ≈ f x) (p : x ≈ y) (q : y ≈ z) : - r ⬝ (ap f (p ⬝ q)) ≈ (r ⬝ ap f p) ⬝ (ap f q) := + definition ap_p_pp (f : A → B) {w x y z : A} (r : f w = f x) (p : x = y) (q : y = z) : + r ⬝ (ap f (p ⬝ q)) = (r ⬝ ap f p) ⬝ (ap f q) := rec_on q (take p, rec_on p (concat_p_pp r idp idp)) p - definition ap_pp_p (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) : - (ap f (p ⬝ q)) ⬝ r ≈ (ap f p) ⬝ (ap f q ⬝ r) := + definition ap_pp_p (f : A → B) {w x y z : A} (p : x = y) (q : y = z) (r : f z = f w) : + (ap f (p ⬝ q)) ⬝ r = (ap f p) ⬝ (ap f q ⬝ r) := rec_on q (rec_on p (take r, concat_pp_p _ _ _)) r -- Functions commute with path inverses. - definition inverse_ap (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)⁻¹ ≈ ap f (p⁻¹) := + definition inverse_ap (f : A → B) {x y : A} (p : x = y) : (ap f p)⁻¹ = ap f (p⁻¹) := rec_on p idp - definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p⁻¹) ≈ (ap f p)⁻¹ := + definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x = y) : ap f (p⁻¹) = (ap f p)⁻¹ := rec_on p idp -- [ap] itself is functorial in the first argument. - definition ap_idmap (p : x ≈ y) : ap id p ≈ p := + definition ap_idmap (p : x = y) : ap id p = p := rec_on p idp - definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : - ap (g ∘ f) p ≈ ap g (ap f p) := + definition ap_compose (f : A → B) (g : B → C) {x y : A} (p : x = y) : + ap (g ∘ f) p = ap g (ap f p) := rec_on p idp -- Sometimes we don't have the actual function [compose]. - definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x ≈ y) : - ap (λa, g (f a)) p ≈ ap g (ap f p) := + definition ap_compose' (f : A → B) (g : B → C) {x y : A} (p : x = y) : + ap (λa, g (f a)) p = ap g (ap f p) := rec_on p idp -- The action of constant maps. - definition ap_const (p : x ≈ y) (z : B) : - ap (λu, z) p ≈ idp := + definition ap_const (p : x = y) (z : B) : + ap (λu, z) p = idp := rec_on p idp -- Naturality of [ap]. - definition concat_Ap {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) : - (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) := + definition concat_Ap {f g : A → B} (p : Π x, f x = g x) {x y : A} (q : x = y) : + (ap f q) ⬝ (p y) = (p x) ⬝ (ap g q) := rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) -- Naturality of [ap] at identity. - definition concat_A1p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) : - (ap f q) ⬝ (p y) ≈ (p x) ⬝ q := + definition concat_A1p {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) : + (ap f q) ⬝ (p y) = (p x) ⬝ q := rec_on q (concat_1p _ ⬝ (concat_p1 _)⁻¹) - definition concat_pA1 {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) : - (p x) ⬝ (ap f q) ≈ q ⬝ (p y) := + definition concat_pA1 {f : A → A} (p : Πx, x = f x) {x y : A} (q : x = y) : + (p x) ⬝ (ap f q) = q ⬝ (p y) := rec_on q (concat_p1 _ ⬝ (concat_1p _)⁻¹) -- Naturality with other paths hanging around. - definition concat_pA_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {w z : B} (r : w ≈ f x) (s : g y ≈ z) : - (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (ap g q ⬝ s) := + definition concat_pA_pp {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) + {w z : B} (r : w = f x) (s : g y = z) : + (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (ap g q ⬝ s) := rec_on s (rec_on q idp) - definition concat_pA_p {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {w : B} (r : w ≈ f x) : - (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ ap g q := + definition concat_pA_p {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) + {w : B} (r : w = f x) : + (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ ap g q := rec_on q idp -- TODO: try this using the simplifier, and compare proofs - definition concat_A_pp {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) - {z : B} (s : g y ≈ z) : - (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (ap g q ⬝ s) := + definition concat_A_pp {f g : A → B} (p : Πx, f x = g x) {x y : A} (q : x = y) + {z : B} (s : g y = z) : + (ap f q) ⬝ (p y ⬝ s) = (p x) ⬝ (ap g q ⬝ s) := rec_on s (rec_on q (calc - (ap f idp) ⬝ (p x ⬝ idp) ≈ idp ⬝ p x : idp - ... ≈ p x : concat_1p _ - ... ≈ (p x) ⬝ (ap g idp ⬝ idp) : idp)) + (ap f idp) ⬝ (p x ⬝ idp) = idp ⬝ p x : idp + ... = p x : concat_1p _ + ... = (p x) ⬝ (ap g idp ⬝ idp) : idp)) -- This also works: -- rec_on s (rec_on q (concat_1p _ ▹ idp)) - definition concat_pA1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {w z : A} (r : w ≈ f x) (s : y ≈ z) : - (r ⬝ ap f q) ⬝ (p y ⬝ s) ≈ (r ⬝ p x) ⬝ (q ⬝ s) := + definition concat_pA1_pp {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) + {w z : A} (r : w = f x) (s : y = z) : + (r ⬝ ap f q) ⬝ (p y ⬝ s) = (r ⬝ p x) ⬝ (q ⬝ s) := rec_on s (rec_on q idp) - definition concat_pp_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {w z : A} (r : w ≈ x) (s : g y ≈ z) : - (r ⬝ p x) ⬝ (ap g q ⬝ s) ≈ (r ⬝ q) ⬝ (p y ⬝ s) := + definition concat_pp_A1p {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) + {w z : A} (r : w = x) (s : g y = z) : + (r ⬝ p x) ⬝ (ap g q ⬝ s) = (r ⬝ q) ⬝ (p y ⬝ s) := rec_on s (rec_on q idp) - definition concat_pA1_p {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {w : A} (r : w ≈ f x) : - (r ⬝ ap f q) ⬝ p y ≈ (r ⬝ p x) ⬝ q := + definition concat_pA1_p {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) + {w : A} (r : w = f x) : + (r ⬝ ap f q) ⬝ p y = (r ⬝ p x) ⬝ q := rec_on q idp - definition concat_A1_pp {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) - {z : A} (s : y ≈ z) : - (ap f q) ⬝ (p y ⬝ s) ≈ (p x) ⬝ (q ⬝ s) := + definition concat_A1_pp {f : A → A} (p : Πx, f x = x) {x y : A} (q : x = y) + {z : A} (s : y = z) : + (ap f q) ⬝ (p y ⬝ s) = (p x) ⬝ (q ⬝ s) := rec_on s (rec_on q (concat_1p _ ▹ idp)) - definition concat_pp_A1 {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {w : A} (r : w ≈ x) : - (r ⬝ p x) ⬝ ap g q ≈ (r ⬝ q) ⬝ p y := + definition concat_pp_A1 {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) + {w : A} (r : w = x) : + (r ⬝ p x) ⬝ ap g q = (r ⬝ q) ⬝ p y := rec_on q idp - definition concat_p_A1p {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y) - {z : A} (s : g y ≈ z) : - p x ⬝ (ap g q ⬝ s) ≈ q ⬝ (p y ⬝ s) := + definition concat_p_A1p {g : A → A} (p : Πx, x = g x) {x y : A} (q : x = y) + {z : A} (s : g y = z) : + p x ⬝ (ap g q ⬝ s) = q ⬝ (p y ⬝ s) := begin apply (rec_on s), apply (rec_on q), @@ -360,27 +357,27 @@ namespace path -- Application of paths between functions preserves the groupoid structure - definition apD10_1 (f : Πx, P x) (x : A) : apD10 (idpath f) x ≈ idp := idp + definition apD10_1 (f : Πx, P x) (x : A) : apD10 (refl f) x = idp := idp - definition apD10_pp {f f' f'' : Πx, P x} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : - apD10 (h ⬝ h') x ≈ apD10 h x ⬝ apD10 h' x := + definition apD10_pp {f f' f'' : Πx, P x} (h : f = f') (h' : f' = f'') (x : A) : + apD10 (h ⬝ h') x = apD10 h x ⬝ apD10 h' x := rec_on h (take h', rec_on h' idp) h' - definition apD10_V {f g : Πx : A, P x} (h : f ≈ g) (x : A) : - apD10 (h⁻¹) x ≈ (apD10 h x)⁻¹ := + definition apD10_V {f g : Πx : A, P x} (h : f = g) (x : A) : + apD10 (h⁻¹) x = (apD10 h x)⁻¹ := rec_on h idp - definition ap10_1 {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp + definition ap10_1 {f : A → B} (x : A) : ap10 (refl f) x = idp := idp - definition ap10_pp {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) : - ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x + definition ap10_pp {f f' f'' : A → B} (h : f = f') (h' : f' = f'') (x : A) : + ap10 (h ⬝ h') x = ap10 h x ⬝ ap10 h' x := apD10_pp h h' x - definition ap10_V {f g : A → B} (h : f ≈ g) (x : A) : ap10 (h⁻¹) x ≈ (ap10 h x)⁻¹ := + definition ap10_V {f g : A → B} (h : f = g) (x : A) : ap10 (h⁻¹) x = (ap10 h x)⁻¹ := apD10_V h x -- [ap10] also behaves nicely on paths produced by [ap] - definition ap_ap10 (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) : - ap h (ap10 p a) ≈ ap10 (ap (λ f', h ∘ f') p) a:= + definition ap_ap10 (f g : A → B) (h : B → C) (p : f = g) (a : A) : + ap h (ap10 p a) = ap10 (ap (λ f', h ∘ f') p) a:= rec_on p idp @@ -388,77 +385,77 @@ namespace path -- --------------------------------------------- definition transport_1 (P : A → Type) {x : A} (u : P x) : - idp ▹ u ≈ u := idp + idp ▹ u = u := idp - definition transport_pp (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) : - p ⬝ q ▹ u ≈ q ▹ p ▹ u := + definition transport_pp (P : A → Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) : + p ⬝ q ▹ u = q ▹ p ▹ u := rec_on q (rec_on p idp) - definition transport_pV (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) : - p ▹ p⁻¹ ▹ z ≈ z := + definition transport_pV (P : A → Type) {x y : A} (p : x = y) (z : P y) : + p ▹ p⁻¹ ▹ z = z := (transport_pp P (p⁻¹) p z)⁻¹ ⬝ ap (λr, transport P r z) (concat_Vp p) - definition transport_Vp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : - p⁻¹ ▹ p ▹ z ≈ z := + definition transport_Vp (P : A → Type) {x y : A} (p : x = y) (z : P x) : + p⁻¹ ▹ p ▹ z = z := (transport_pp P p (p⁻¹) z)⁻¹ ⬝ ap (λr, transport P r z) (concat_pV p) definition transport_p_pp (P : A → Type) - {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : + {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) : ap (λe, e ▹ u) (concat_p_pp p q r) ⬝ (transport_pp P (p ⬝ q) r u) ⬝ ap (transport P r) (transport_pp P p q u) - ≈ (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u)) - :> ((p ⬝ (q ⬝ r)) ▹ u ≈ r ▹ q ▹ p ▹ u) := + = (transport_pp P p (q ⬝ r) u) ⬝ (transport_pp P q r (p ▹ u)) + :> ((p ⬝ (q ⬝ r)) ▹ u = r ▹ q ▹ p ▹ u) := rec_on r (rec_on q (rec_on p idp)) -- Here is another coherence lemma for transport. - definition transport_pVp (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : - transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) := + definition transport_pVp (P : A → Type) {x y : A} (p : x = y) (z : P x) : + transport_pV P p (transport P p z) = ap (transport P p) (transport_Vp P p z) := rec_on p idp -- Dependent transport in a doubly dependent type. -- should P, Q and y all be explicit here? definition transportD (P : A → Type) (Q : Π a : A, P a → Type) - {a a' : A} (p : a ≈ a') (b : P a) (z : Q a b) : Q a' (p ▹ b) := + {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) := rec_on p z -- In Coq the variables B, C and y are explicit, but in Lean we can probably have them implicit using the following notation notation p `▹D`:65 x:64 := transportD _ _ p _ x -- Transporting along higher-dimensional paths - definition transport2 (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : - p ▹ z ≈ q ▹ z := + definition transport2 (P : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : P x) : + p ▹ z = q ▹ z := ap (λp', p' ▹ z) r notation p `▹2`:65 x:64 := transport2 _ p _ x -- An alternative definition. - definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) + definition transport2_is_ap10 (Q : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) : - transport2 Q r z ≈ ap10 (ap (transport Q) r) z := + transport2 Q r z = ap10 (ap (transport Q) r) z := rec_on r idp - definition transport2_p2p (P : A → Type) {x y : A} {p1 p2 p3 : x ≈ y} - (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) (z : P x) : - transport2 P (r1 ⬝ r2) z ≈ transport2 P r1 z ⬝ transport2 P r2 z := + definition transport2_p2p (P : A → Type) {x y : A} {p1 p2 p3 : x = y} + (r1 : p1 = p2) (r2 : p2 = p3) (z : P x) : + transport2 P (r1 ⬝ r2) z = transport2 P r1 z ⬝ transport2 P r2 z := rec_on r1 (rec_on r2 idp) - definition transport2_V (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) : - transport2 Q (r⁻¹) z ≈ ((transport2 Q r z)⁻¹) := + definition transport2_V (Q : A → Type) {x y : A} {p q : x = y} (r : p = q) (z : Q x) : + transport2 Q (r⁻¹) z = ((transport2 Q r z)⁻¹) := rec_on r idp definition transportD2 (B C : A → Type) (D : Π(a:A), B a → C a → Type) - {x1 x2 : A} (p : x1 ≈ x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) := + {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z) : D x2 (p ▹ y) (p ▹ z) := rec_on p w notation p `▹D2`:65 x:64 := transportD2 _ _ _ p _ _ x - definition concat_AT (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q) - (s : z ≈ w) : - ap (transport P p) s ⬝ transport2 P r w ≈ transport2 P r z ⬝ ap (transport P q) s := + definition concat_AT (P : A → Type) {x y : A} {p q : x = y} {z w : P x} (r : p = q) + (s : z = w) : + ap (transport P p) s ⬝ transport2 P r w = transport2 P r z ⬝ ap (transport P q) s := rec_on r (concat_p1 _ ⬝ (concat_1p _)⁻¹) -- TODO (from Coq library): What should this be called? - definition ap_transport {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) : - f y (p ▹ z) ≈ (p ▹ (f x z)) := + definition ap_transport {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) : + f y (p ▹ z) = (p ▹ (f x z)) := rec_on p idp @@ -475,34 +472,34 @@ namespace path -/ -- Transporting in a constant fibration. - definition transport_const (p : x ≈ y) (z : B) : transport (λx, B) p z ≈ z := + definition transport_const (p : x = y) (z : B) : transport (λx, B) p z = z := rec_on p idp - definition transport2_const {p q : x ≈ y} (r : p ≈ q) (z : B) : - transport_const p z ≈ transport2 (λu, B) r z ⬝ transport_const q z := + definition transport2_const {p q : x = y} (r : p = q) (z : B) : + transport_const p z = transport2 (λu, B) r z ⬝ transport_const q z := rec_on r (concat_1p _)⁻¹ -- Transporting in a pulled back fibration. -- TODO: P can probably be implicit - definition transport_compose (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) : - transport (P ∘ f) p z ≈ transport P (ap f p) z := + definition transport_compose (P : B → Type) (f : A → B) (p : x = y) (z : P (f x)) : + transport (P ∘ f) p z = transport P (ap f p) z := rec_on p idp - definition transport_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') : - transport (λh : B → C, g ∘ f ≈ h ∘ f) p idp ≈ ap (λh, h ∘ f) p := + definition transport_precompose (f : A → B) (g g' : B → C) (p : g = g') : + transport (λh : B → C, g ∘ f = h ∘ f) p idp = ap (λh, h ∘ f) p := rec_on p idp - definition apD10_ap_precompose (f : A → B) (g g' : B → C) (p : g ≈ g') (a : A) : - apD10 (ap (λh : B → C, h ∘ f) p) a ≈ apD10 p (f a) := + definition apD10_ap_precompose (f : A → B) (g g' : B → C) (p : g = g') (a : A) : + apD10 (ap (λh : B → C, h ∘ f) p) a = apD10 p (f a) := rec_on p idp - definition apD10_ap_postcompose (f : B → C) (g g' : A → B) (p : g ≈ g') (a : A) : - apD10 (ap (λh : A → B, f ∘ h) p) a ≈ ap f (apD10 p a) := + definition apD10_ap_postcompose (f : B → C) (g g' : A → B) (p : g = g') (a : A) : + apD10 (ap (λh : A → B, f ∘ h) p) a = ap f (apD10 p a) := rec_on p idp -- A special case of [transport_compose] which seems to come up a lot. - definition transport_idmap_ap (P : A → Type) x y (p : x ≈ y) (u : P x) : - transport P p u ≈ transport (λz, z) (ap P p) u := + definition transport_idmap_ap (P : A → Type) x y (p : x = y) (u : P x) : + transport P p u = transport (λz, z) (ap P p) u := rec_on p idp @@ -510,8 +507,8 @@ namespace path -- ------------------------------ -- In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. - definition apD_const (f : A → B) (p: x ≈ y) : - apD f p ≈ transport_const p (f x) ⬝ ap f p := + definition apD_const (f : A → B) (p: x = y) : + apD f p = transport_const p (f x) ⬝ ap f p := rec_on p idp @@ -519,87 +516,87 @@ namespace path -- ------------------------------------ -- Horizontal composition of 2-dimensional paths. - definition concat2 {p p' : x ≈ y} {q q' : y ≈ z} (h : p ≈ p') (h' : q ≈ q') : - p ⬝ q ≈ p' ⬝ q' := + definition concat2 {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') : + p ⬝ q = p' ⬝ q' := rec_on h (rec_on h' idp) infixl `◾`:75 := concat2 -- 2-dimensional path inversion - definition inverse2 {p q : x ≈ y} (h : p ≈ q) : p⁻¹ ≈ q⁻¹ := + definition inverse2 {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ := rec_on h idp -- Whiskering -- ---------- - definition whiskerL (p : x ≈ y) {q r : y ≈ z} (h : q ≈ r) : p ⬝ q ≈ p ⬝ r := + definition whiskerL (p : x = y) {q r : y = z} (h : q = r) : p ⬝ q = p ⬝ r := idp ◾ h - definition whiskerR {p q : x ≈ y} (h : p ≈ q) (r : y ≈ z) : p ⬝ r ≈ q ⬝ r := + definition whiskerR {p q : x = y} (h : p = q) (r : y = z) : p ⬝ r = q ⬝ r := h ◾ idp -- Unwhiskering, a.k.a. cancelling - definition cancelL {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) := + definition cancelL {x y z : A} (p : x = y) (q r : y = z) : (p ⬝ q = p ⬝ r) → (q = r) := rec_on p (take r, rec_on r (take q a, (concat_1p q)⁻¹ ⬝ a)) r q - definition cancelR {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) := + definition cancelR {x y z : A} (p q : x = y) (r : y = z) : (p ⬝ r = q ⬝ r) → (p = q) := rec_on r (rec_on p (take q a, a ⬝ concat_p1 q)) q -- Whiskering and identity paths. - definition whiskerR_p1 {p q : x ≈ y} (h : p ≈ q) : - (concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h := + definition whiskerR_p1 {p q : x = y} (h : p = q) : + (concat_p1 p)⁻¹ ⬝ whiskerR h idp ⬝ concat_p1 q = h := rec_on h (rec_on p idp) - definition whiskerR_1p (p : x ≈ y) (q : y ≈ z) : - whiskerR idp q ≈ idp :> (p ⬝ q ≈ p ⬝ q) := + definition whiskerR_1p (p : x = y) (q : y = z) : + whiskerR idp q = idp :> (p ⬝ q = p ⬝ q) := rec_on q idp - definition whiskerL_p1 (p : x ≈ y) (q : y ≈ z) : - whiskerL p idp ≈ idp :> (p ⬝ q ≈ p ⬝ q) := + definition whiskerL_p1 (p : x = y) (q : y = z) : + whiskerL p idp = idp :> (p ⬝ q = p ⬝ q) := rec_on q idp - definition whiskerL_1p {p q : x ≈ y} (h : p ≈ q) : - (concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h := + definition whiskerL_1p {p q : x = y} (h : p = q) : + (concat_1p p) ⁻¹ ⬝ whiskerL idp h ⬝ concat_1p q = h := rec_on h (rec_on p idp) - definition concat2_p1 {p q : x ≈ y} (h : p ≈ q) : - h ◾ idp ≈ whiskerR h idp :> (p ⬝ idp ≈ q ⬝ idp) := + definition concat2_p1 {p q : x = y} (h : p = q) : + h ◾ idp = whiskerR h idp :> (p ⬝ idp = q ⬝ idp) := rec_on h idp - definition concat2_1p {p q : x ≈ y} (h : p ≈ q) : - idp ◾ h ≈ whiskerL idp h :> (idp ⬝ p ≈ idp ⬝ q) := + definition concat2_1p {p q : x = y} (h : p = q) : + idp ◾ h = whiskerL idp h :> (idp ⬝ p = idp ⬝ q) := rec_on h idp -- TODO: note, 4 inductions -- The interchange law for concatenation. - definition concat_concat2 {p p' p'' : x ≈ y} {q q' q'' : y ≈ z} - (a : p ≈ p') (b : p' ≈ p'') (c : q ≈ q') (d : q' ≈ q'') : - (a ◾ c) ⬝ (b ◾ d) ≈ (a ⬝ b) ◾ (c ⬝ d) := + definition concat_concat2 {p p' p'' : x = y} {q q' q'' : y = z} + (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') : + (a ◾ c) ⬝ (b ◾ d) = (a ⬝ b) ◾ (c ⬝ d) := rec_on d (rec_on c (rec_on b (rec_on a idp))) - definition concat_whisker {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') : - (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') := + definition concat_whisker {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') : + (whiskerR a q) ⬝ (whiskerL p' b) = (whiskerL p b) ⬝ (whiskerR a q') := rec_on b (rec_on a (concat_1p _)⁻¹) -- Structure corresponding to the coherence equations of a bicategory. -- The "pentagonator": the 3-cell witnessing the associativity pentagon. - definition pentagon {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z) : + definition pentagon {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z) : whiskerL p (concat_p_pp q r s) ⬝ concat_p_pp p (q ⬝ r) s ⬝ whiskerR (concat_p_pp p q r) s - ≈ concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := + = concat_p_pp p q (r ⬝ s) ⬝ concat_p_pp (p ⬝ q) r s := rec_on s (rec_on r (rec_on q (rec_on p idp))) -- The 3-cell witnessing the left unit triangle. - definition triangulator (p : x ≈ y) (q : y ≈ z) : - concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q ≈ whiskerL p (concat_1p q) := + definition triangulator (p : x = y) (q : y = z) : + concat_p_pp p idp q ⬝ whiskerR (concat_p1 p) q = whiskerL p (concat_1p q) := rec_on q (rec_on p idp) - definition eckmann_hilton {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p := + definition eckmann_hilton {x:A} (p q : idp = idp :> (x = x)) : p ⬝ q = q ⬝ p := (!whiskerR_p1 ◾ !whiskerL_1p)⁻¹ ⬝ (!concat_p1 ◾ !concat_p1) ⬝ (!concat_1p ◾ !concat_1p) @@ -609,51 +606,52 @@ namespace path ⬝ (!whiskerL_1p ◾ !whiskerR_p1) -- The action of functions on 2-dimensional paths - definition ap02 (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q := + definition ap02 (f:A → B) {x y : A} {p q : x = y} (r : p = q) : ap f p = ap f q := rec_on r idp - definition ap02_pp (f : A → B) {x y : A} {p p' p'' : x ≈ y} (r : p ≈ p') (r' : p' ≈ p'') : - ap02 f (r ⬝ r') ≈ ap02 f r ⬝ ap02 f r' := + definition ap02_pp (f : A → B) {x y : A} {p p' p'' : x = y} (r : p = p') (r' : p' = p'') : + ap02 f (r ⬝ r') = ap02 f r ⬝ ap02 f r' := rec_on r (rec_on r' idp) - definition ap02_p2p (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈ z} (r : p ≈ p') - (s : q ≈ q') : - ap02 f (r ◾ s) ≈ ap_pp f p q + definition ap02_p2p (f : A → B) {x y z : A} {p p' : x = y} {q q' :y = z} (r : p = p') + (s : q = q') : + ap02 f (r ◾ s) = ap_pp f p q ⬝ (ap02 f r ◾ ap02 f s) ⬝ (ap_pp f p' q')⁻¹ := rec_on r (rec_on s (rec_on q (rec_on p idp))) -- rec_on r (rec_on s (rec_on p (rec_on q idp))) - definition apD02 {p q : x ≈ y} (f : Π x, P x) (r : p ≈ q) : - apD f p ≈ transport2 P r (f x) ⬝ apD f q := + definition apD02 {p q : x = y} (f : Π x, P x) (r : p = q) : + apD f p = transport2 P r (f x) ⬝ apD f q := rec_on r (concat_1p _)⁻¹ -- And now for a lemma whose statement is much longer than its proof. definition apD02_pp (P : A → Type) (f : Π x:A, P x) {x y : A} - {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3) : - apD02 f (r1 ⬝ r2) ≈ apD02 f r1 + {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3) : + apD02 f (r1 ⬝ r2) = apD02 f r1 ⬝ whiskerL (transport2 P r1 (f x)) (apD02 f r2) ⬝ concat_p_pp _ _ _ ⬝ (whiskerR ((transport2_p2p P r1 r2 (f x))⁻¹) (apD f p3)) := rec_on r2 (rec_on r1 (rec_on p1 idp)) -end path -namespace path +end eq + +namespace eq variables {A B C D E : Type} {a a' : A} {b b' : B} {c c' : C} {d d' : D} -theorem congr_arg2 (f : A → B → C) (Ha : a ≈ a') (Hb : b ≈ b') : f a b ≈ f a' b' := +theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' := rec_on Ha (rec_on Hb idp) -theorem congr_arg3 (f : A → B → C → D) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c') - : f a b c ≈ f a' b' c' := +theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') + : f a b c = f a' b' c' := rec_on Ha (congr_arg2 (f a) Hb Hc) -theorem congr_arg4 (f : A → B → C → D → E) (Ha : a ≈ a') (Hb : b ≈ b') (Hc : c ≈ c') (Hd : d ≈ d') - : f a b c d ≈ f a' b' c' d' := +theorem congr_arg4 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') + : f a b c d = f a' b' c' d' := rec_on Ha (congr_arg3 (f a) Hb Hc Hd) -end path +end eq -namespace path +namespace eq variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {E : Πa b c, D a b c → Type} {F : Type} variables {a a' : A} @@ -661,8 +659,8 @@ variables {a a' : A} {c : C a b} {c' : C a' b'} {d : D a b c} {d' : D a' b' c'} -theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a ≈ a') (Hb : Ha ▹ b ≈ b') - : f a b ≈ f a' b' := +theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : (Ha ▹ b) = b') + : f a b = f a' b' := rec_on Hb (rec_on Ha idp) /- From the Coq version: @@ -717,4 +715,4 @@ rec_on Hb (rec_on Ha idp) autorewrite with paths in * |- * ; auto with path_hints. -/ -end path +end eq diff --git a/hott/trunc.hlean b/hott/init/trunc.hlean similarity index 87% rename from hott/trunc.hlean rename to hott/init/trunc.hlean index 8c9617f18..c4093033d 100644 --- a/hott/trunc.hlean +++ b/hott/init/trunc.hlean @@ -2,9 +2,9 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Jeremy Avigad, Floris van Doorn -- Ported from Coq HoTT - -import .path .logic data.nat.basic data.empty data.unit data.sigma .equiv -open path nat sigma unit +prelude +import .path .logic .datatypes .equiv .types.empty .types.sigma +open eq nat sigma unit set_option pp.universes true -- Truncation levels @@ -59,11 +59,11 @@ namespace truncation -/ structure contr_internal (A : Type) := - (center : A) (contr : Π(a : A), center ≈ a) + (center : A) (contr : Π(a : A), center = a) 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))) + (λn trunc_n A, (Π(x y : A), trunc_n (x = y))) structure is_trunc [class] (n : trunc_index) (A : Type) := (to_internal : is_trunc_internal n A) @@ -79,33 +79,33 @@ namespace truncation variables {A B : Type} -- TODO: rename to is_trunc_succ - 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) -- TODO: rename to is_trunc_path - definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) := + definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x = y) := is_trunc.mk (!is_trunc.to_internal x y) /- contractibility -/ - definition is_contr.mk (center : A) (contr : Π(a : A), center ≈ a) : is_contr A := + 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 := @contr_internal.center A !is_trunc.to_internal - definition contr [H : is_contr A] (a : A) : !center ≈ a := + definition contr [H : is_contr A] (a : A) : !center = a := @contr_internal.contr A !is_trunc.to_internal a - definition path_contr [H : is_contr A] (x y : A) : x ≈ y := + 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 := - have K : ∀ (r : x ≈ y), path_contr x y ≈ r, from (λ r, path.rec_on r !concat_Vp), + 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, eq.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 -/ @@ -132,7 +132,7 @@ namespace truncation λm IHm n, trunc_index.rec_on n (λA Hnm Hn, @trunc_succ A m (IHm -2 A star Hn)) (λn IHn A Hnm (Hn : is_trunc n.+1 A), - @is_trunc_succ A m (λx y, IHm n (x≈y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)), + @is_trunc_succ A m (λx y, IHm n (x = y) (trunc_index.succ_le_cancel Hnm) !succ_is_trunc)), trunc_index.rec_on m base step n A Hnm Hn -- the following cannot be instances in their current form, because it is looping @@ -145,11 +145,11 @@ namespace truncation definition trunc_hset (A : Type) (n : trunc_index) [H : is_hset A] : is_trunc (n.+2) A := - trunc_leq A 0 (n.+2) star + trunc_leq A nat.zero (n.+2) star /- hprops -/ - definition is_hprop.elim [H : is_hprop A] (x y : A) : x ≈ y := + 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 := @@ -162,21 +162,21 @@ namespace truncation 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 := + definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q := @is_hprop.elim _ !succ_is_trunc p q /- instances -/ - 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 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, eq.rec_on q idp)) -- definition is_trunc_is_hprop [instance] {n : trunc_index} : is_hprop (is_trunc n A) := sorry @@ -197,7 +197,7 @@ namespace truncation notation `hset` := 0-Type definition hprop.mk := @trunctype.mk -1 - definition hset.mk := @trunctype.mk 0 + definition hset.mk := @trunctype.mk nat.zero --what does the following line in Coq do? --Canonical Structure default_TruncType := fun n T P => (@BuildTruncType n T P). @@ -224,7 +224,7 @@ namespace truncation trunc_index.rec_on n (λA (HA : is_contr A) B f (H : is_equiv f), !equiv_preserves_contr) (λn IH A (HA : is_trunc n.+1 A) B f (H : is_equiv f), @is_trunc_succ _ _ (λ x y : B, - IH (f⁻¹ x ≈ f⁻¹ y) !succ_is_trunc (x ≈ y) ((ap (f⁻¹))⁻¹) !inv_closed)) + IH (f⁻¹ x = f⁻¹ y) !succ_is_trunc (x = y) ((ap (f⁻¹))⁻¹) !inv_closed)) A HA B f H definition trunc_equiv' (n : trunc_index) (f : A ≃ B) [HA : is_trunc n A] : is_trunc n B := diff --git a/hott/init/types/empty.hlean b/hott/init/types/empty.hlean new file mode 100644 index 000000000..383e234b8 --- /dev/null +++ b/hott/init/types/empty.hlean @@ -0,0 +1,36 @@ +-- Copyright (c) 2014 Microsoft Corporation. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Jeremy Avigad, Floris van Doorn, Jakob von Raumer + +prelude +import ..datatypes ..logic +-- Empty type +-- ---------- + +namespace empty + protected theorem elim (A : Type) (H : empty) : A := + rec (λe, A) H +end empty + +protected definition empty.has_decidable_eq [instance] : decidable_eq empty := +take (a b : empty), decidable.inl (!empty.elim a) + +definition tneg.tneg (A : Type) := A → empty +prefix `~` := tneg.tneg +namespace tneg +variables {A B : Type} +protected definition intro (H : A → empty) : ~A := H +protected definition elim (H1 : ~A) (H2 : A) : empty := H1 H2 +protected definition empty : ~empty := λH : empty, H +definition tabsurd (H1 : A) (H2 : ~A) : B := !empty.elim (H2 H1) +definition tneg_tneg_intro (H : A) : ~~A := λH2 : ~A, tneg.elim H2 H +definition tmt (H1 : A → B) (H2 : ~B) : ~A := λHA : A, tabsurd (H1 HA) H2 + +definition tneg_pi_left {B : A → Type} (H : ~Πa, B a) : ~~A := +λHnA : ~A, tneg.elim H (λHA : A, tabsurd HA HnA) + +definition tneg_function_right (H : ~(A → B)) : ~B := +λHB : B, tneg.elim H (λHA : A, HB) + + +end tneg diff --git a/hott/init/prod.hlean b/hott/init/types/prod.hlean similarity index 97% rename from hott/init/prod.hlean rename to hott/init/types/prod.hlean index 4528f1d5a..e9cb0fa87 100644 --- a/hott/init/prod.hlean +++ b/hott/init/types/prod.hlean @@ -6,7 +6,7 @@ Module: data.prod.decl Author: Leonardo de Moura, Jeremy Avigad -/ prelude -import init.wf +import ..wf definition pair := @prod.mk @@ -18,6 +18,8 @@ namespace prod infixr `*` := prod end low_precedence_times + definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a) + notation `pr₁` := pr1 notation `pr₂` := pr2 @@ -80,4 +82,5 @@ namespace prod subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb) end + end prod diff --git a/hott/init/sigma.hlean b/hott/init/types/sigma.hlean similarity index 92% rename from hott/init/sigma.hlean rename to hott/init/types/sigma.hlean index 8b2c55f70..ce2324acd 100644 --- a/hott/init/sigma.hlean +++ b/hott/init/types/sigma.hlean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ prelude -import init.num init.wf init.logic init.tactic +import ..num ..wf ..logic ..tactic structure sigma {A : Type} (B : A → Type) := dpair :: (dpr1 : A) (dpr2 : B dpr1) diff --git a/hott/logic.hlean b/hott/logic.hlean index bd41ed824..2660e3e7c 100644 --- a/hott/logic.hlean +++ b/hott/logic.hlean @@ -1,9 +1,9 @@ -import data.empty .path +--javra: Maybe this should go somewhere else -open path +open eq inductive tdecidable [class] (A : Type) : Type := inl : A → tdecidable A, inr : ~A → tdecidable A structure decidable_paths [class] (A : Type) := -(elim : ∀(x y : A), tdecidable (x ≈ y)) +(elim : ∀(x y : A), tdecidable (x = y)) diff --git a/hott/pointed.hlean b/hott/pointed.hlean index e5d633286..7682c1833 100644 --- a/hott/pointed.hlean +++ b/hott/pointed.hlean @@ -2,9 +2,8 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Jakob von Raumer -- Ported from Coq HoTT -import hott.path hott.trunc data.sigma data.prod - -open path prod truncation +import init.trunc +open eq prod truncation structure is_pointed [class] (A : Type) := (point : A) @@ -30,7 +29,7 @@ namespace is_pointed : is_pointed (A × B) := is_pointed.mk (prod.mk (point A) (point B)) - protected definition loop_space (a : A) : is_pointed (a ≈ a) := + protected definition loop_space (a : A) : is_pointed (a = a) := is_pointed.mk idp end is_pointed diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 6ce45403e..77e4291b0 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -6,9 +6,8 @@ Ported from Coq HoTT Theorems about pi-types (dependent function spaces) -/ - -import ..trunc ..axioms.funext .sigma -open path equiv is_equiv funext +import init.equiv init.axioms.funext types.sigma +open eq equiv is_equiv funext namespace pi universe variables l k @@ -27,45 +26,45 @@ namespace pi 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 := + 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, idpath (f x)) ≈ idpath f := + 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) := + 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) := + 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) + 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)))) := - path.rec_on p (λx, idp) + 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) - : (path.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, path.transport (λa, C a b) p (f b)) := - path.rec_on p (λx, idp) + 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) := + 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 (path.rec_on p), + apply (eq.rec_on p), apply inverse, apply path_pi_idp end @@ -73,20 +72,20 @@ namespace pi /- Dependent paths -/ /- with more implicit arguments the conclusion of the following theorem is - (Π(b : B a), transportD B C p b (f b) ≈ g (path.transport B p b)) ≃ - (path.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) := - path.rec_on p (λg, !homotopy_equiv_path) g + (Π(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.ops /- more implicit arguments: - (Π(b : B a), path.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 (path.transport B p b)) -/ - definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a ≈ a') + (Π(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)) := - path.rec_on p (λg, !equiv.refl) g + (Π(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 /- truncation -/ @@ -108,12 +107,12 @@ namespace pi apply equiv.symm, apply path_equiv_homotopy, apply IH, intro a, - show is_trunc n (f a ≈ g a), from + show is_trunc n (f a = g a), from succ_is_trunc n (f a) (g a) end definition trunc_path_pi [instance] [H : funext.{l k}] (n : trunc_index) (f g : Πa, B a) - [H : ∀a, is_trunc n (f a ≈ g a)] : is_trunc n (f ≈ g) := + [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) := begin apply trunc_equiv', apply equiv.symm, apply path_equiv_homotopy, diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 97ccc51ea..9ccf6b2fa 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -7,8 +7,8 @@ Ported from Coq HoTT Theorems about products -/ -import ..trunc data.prod -open path equiv is_equiv truncation prod +import init.trunc init.datatypes +open eq equiv is_equiv truncation prod variables {A A' B B' C D : Type} {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B} @@ -16,13 +16,13 @@ variables {A A' B B' C D : Type} namespace prod -- prod.eta is already used for the eta rule for strict equality - protected definition peta (u : A × B) : (pr₁ u , pr₂ u) ≈ u := + protected definition peta (u : A × B) : (pr₁ u , pr₂ u) = u := destruct u (λu1 u2, idp) - definition pair_path (pa : a ≈ a') (pb : b ≈ b') : (a , b) ≈ (a' , b') := - path.rec_on pa (path.rec_on pb idp) + definition pair_path (pa : a = a') (pb : b = b') : (a , b) = (a' , b') := + eq.rec_on pa (eq.rec_on pb idp) - protected definition path : (pr₁ u ≈ pr₁ v) → (pr₂ u ≈ pr₂ v) → u ≈ v := + protected definition path : (pr₁ u = pr₁ v) → (pr₂ u = pr₂ v) → u = v := begin apply (prod.rec_on u), intros (a₁, b₁), apply (prod.rec_on v), intros (a₂, b₂, H₁, H₂), diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index a35f3ff9f..c7730694a 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -7,8 +7,8 @@ Ported from Coq HoTT Theorems about sigma-types (dependent sums) -/ -import ..trunc .prod ..axioms.funext -open path sigma sigma.ops equiv is_equiv +import init.trunc init.axioms.funext init.types.prod +open eq sigma sigma.ops equiv is_equiv namespace sigma infixr [local] ∘ := function.compose --remove @@ -17,95 +17,95 @@ namespace sigma {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a} -- sigma.eta is already used for the eta rule for strict equality - protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ ≈ u := + protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ = u := destruct u (λu1 u2, idp) - definition eta2 (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ ≈ u := + definition eta2 (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 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ ≈ u := + definition eta3 (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 dpair_eq_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 + definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' := + eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q /- In Coq they often have to give u and v explicitly -/ - protected definition path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v := + protected definition path (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : u = v := destruct u (λu1 u2, destruct v (λ v1 v2, dpair_eq_dpair)) p q /- Projections of paths from a total space -/ - definition path_pr1 (p : u ≈ v) : u.1 ≈ v.1 := + definition path_pr1 (p : u = v) : u.1 = v.1 := ap dpr1 p postfix `..1`:(max+1) := path_pr1 - definition path_pr2 (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 := - path.rec_on p idp + definition path_pr2 (p : u = v) : p..1 ▹ u.2 = v.2 := + eq.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`:(max+1) := path_pr2 - definition dpair_sigma_path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) - : dpair (sigma.path p q)..1 (sigma.path p q)..2 ≈ ⟨p, q⟩ := + definition dpair_sigma_path (p : u.1 = v.1) (q : p ▹ u.2 = v.2) + : dpair (sigma.path p q)..1 (sigma.path p q)..2 = ⟨p, q⟩ := begin reverts (p, q), apply (destruct u), intros (u1, u2), apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert - apply (path.rec_on p), intros (v2, q), - apply (path.rec_on q), apply idp + apply (eq.rec_on p), intros (v2, q), + apply (eq.rec_on q), apply idp end - definition sigma_path_pr1 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (sigma.path p q)..1 ≈ p := + definition sigma_path_pr1 (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : (sigma.path p q)..1 = p := (!dpair_sigma_path)..1 - definition sigma_path_pr2 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) - : sigma_path_pr1 p q ▹ (sigma.path p q)..2 ≈ q := + definition sigma_path_pr2 (p : u.1 = v.1) (q : p ▹ u.2 = v.2) + : sigma_path_pr1 p q ▹ (sigma.path p q)..2 = q := (!dpair_sigma_path)..2 - definition sigma_path_eta (p : u ≈ v) : sigma.path (p..1) (p..2) ≈ p := + definition sigma_path_eta (p : u = v) : sigma.path (p..1) (p..2) = p := begin - apply (path.rec_on p), + apply (eq.rec_on p), apply (destruct u), intros (u1, u2), apply idp end - definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) - : transport (λx, B' x.1) (sigma.path p q) ≈ transport B' p := + definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 = v.1) (q : p ▹ u.2 = v.2) + : transport (λx, B' x.1) (sigma.path p q) = transport B' p := begin reverts (p, q), 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 + apply (eq.rec_on p), intros (v2, q), + apply (eq.rec_on q), apply idp end - /- the uncurried version of sigma_path. We will prove that this is an equivalence -/ + /- the uncurried version of sigma_eq. We will prove that this is an equivalence -/ - definition sigma_path_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v := + definition sigma_path_uncurried (pq : Σ(p : dpr1 u = dpr1 v), p ▹ (dpr2 u) = dpr2 v) : u = v := destruct pq sigma.path - definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) - : dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 ≈ pq := + definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2) + : dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 = pq := destruct pq dpair_sigma_path - definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) - : (sigma_path_uncurried pq)..1 ≈ pq.1 := + definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2) + : (sigma_path_uncurried pq)..1 = pq.1 := (!dpair_sigma_path_uncurried)..1 - definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) - : (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 ≈ pq.2 := + definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2) + : (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 = pq.2 := (!dpair_sigma_path_uncurried)..2 - definition sigma_path_eta_uncurried (p : u ≈ v) : sigma_path_uncurried (dpair p..1 p..2) ≈ p := + definition sigma_path_eta_uncurried (p : u = v) : sigma_path_uncurried (dpair p..1 p..2) = p := !sigma_path_eta definition transport_sigma_path_dpr1_uncurried {B' : A → Type} - (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) - : transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) ≈ transport B' pq.1 := + (pq : Σ(p : u.1 = v.1), p ▹ u.2 = v.2) + : transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) = transport B' pq.1 := destruct pq transport_dpr1_sigma_path definition is_equiv_sigma_path [instance] (u v : Σa, B a) @@ -115,25 +115,25 @@ namespace sigma sigma_path_eta_uncurried dpair_sigma_path_uncurried - definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2) ≃ (u ≈ v) := + definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 = v.1), p ▹ u.2 = v.2) ≃ (u = v) := equiv.mk sigma_path_uncurried !is_equiv_sigma_path - definition dpair_eq_dpair_pp_pp (p1 : a ≈ a' ) (q1 : p1 ▹ b ≈ b' ) - (p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') : + definition dpair_eq_dpair_pp_pp (p1 : a = a' ) (q1 : p1 ▹ b = b' ) + (p2 : a' = a'') (q2 : p2 ▹ b' = b'') : dpair_eq_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2) - ≈ dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 := + = dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair p2 q2 := begin reverts (b', p2, b'', q1, q2), - 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 + apply (eq.rec_on p1), intros (b', p2), + apply (eq.rec_on p2), intros (b'', q1), + apply (eq.rec_on q1), intro q2, + apply (eq.rec_on q2), apply idp end - definition sigma_path_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2) - (p2 : v.1 ≈ w.1) (q2 : p2 ▹ v.2 ≈ w.2) : + definition sigma_path_pp_pp (p1 : u.1 = v.1) (q1 : p1 ▹ u.2 = v.2) + (p2 : v.1 = w.1) (q2 : p2 ▹ v.2 = w.2) : sigma.path (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2) - ≈ sigma.path p1 q1 ⬝ sigma.path p2 q2 := + = sigma.path p1 q1 ⬝ sigma.path p2 q2 := begin reverts (p1, q1, p2, q2), apply (destruct u), intros (u1, u2), @@ -142,49 +142,49 @@ namespace sigma apply dpair_eq_dpair_pp_pp end - definition dpair_eq_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') : - dpair_eq_dpair p q ≈ dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q := + definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') : + dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q := begin reverts (b', q), - apply (path.rec_on p), intros (b', q), - apply (path.rec_on q), apply idp + apply (eq.rec_on p), intros (b', q), + apply (eq.rec_on q), apply idp end /- path_pr1 commutes with the groupoid structure. -/ - definition path_pr1_idp (u : Σa, B a) : (idpath u)..1 ≈ idpath (u.1) := idp - definition path_pr1_pp (p : u ≈ v) (q : v ≈ w) : (p ⬝ q) ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp - definition path_pr1_V (p : u ≈ v) : p⁻¹ ..1 ≈ (p..1)⁻¹ := !ap_V + definition path_pr1_idp (u : Σa, B a) : (refl u)..1 = refl (u.1) := idp + definition path_pr1_pp (p : u = v) (q : v = w) : (p ⬝ q) ..1 = (p..1) ⬝ (q..1) := !ap_pp + definition path_pr1_V (p : u = v) : p⁻¹ ..1 = (p..1)⁻¹ := !ap_V /- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/ - definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ dpair_eq_dpair idp q := - path.rec_on q idp + definition ap_dpair (q : b₁ = b₂) : ap (dpair a) q = dpair_eq_dpair idp q := + eq.rec_on q idp - /- Dependent transport is the same as transport along a sigma_path. -/ + /- Dependent transport is the same as transport along a sigma_eq. -/ - definition transportD_eq_transport (p : a ≈ a') (c : C a b) : - p ▹D c ≈ transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c := - path.rec_on p idp + definition transportD_eq_transport (p : a = a') (c : C a b) : + p ▹D c = transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c := + eq.rec_on p idp - definition sigma_path_eq_sigma_path {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'} - (r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : sigma.path p1 p2 ≈ sigma.path q1 q2 := - path.rec_on r - proof (λq2 s, path.rec_on s idp) qed + definition sigma_path_eq_sigma_path {p1 q1 : a = a'} {p2 : p1 ▹ b = b'} {q2 : q1 ▹ b = b'} + (r : p1 = q1) (s : r ▹ p2 = q2) : sigma.path p1 p2 = sigma.path q1 q2 := + eq.rec_on r + proof (λq2 s, eq.rec_on s idp) qed q2 s -- begin -- reverts (q2, s), - -- apply (path.rec_on r), intros (q2, s), - -- apply (path.rec_on s), apply idp + -- apply (eq.rec_on r), intros (q2, s), + -- apply (eq.rec_on s), apply idp -- end /- A path between paths in a total space is commonly shown component wise. -/ - definition path_sigma_path {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q := + definition path_sigma_path {p q : u = v} (r : p..1 = q..1) (s : r ▹ p..2 = q..2) : p = q := begin reverts (q, r, s), - apply (path.rec_on p), + apply (eq.rec_on p), apply (destruct u), intros (u1, u2, q, r, s), apply concat, rotate 1, apply sigma_path_eta, @@ -192,8 +192,8 @@ namespace sigma end /- In Coq they often have to give u and v explicitly when using the following definition -/ - definition path_sigma_path_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 := + definition path_sigma_path_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_sigma_path /- Transport -/ @@ -202,30 +202,30 @@ namespace sigma 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_eq (p : a ≈ a') (bc : Σ(b : B a), C a b) - : p ▹ bc ≈ ⟨p ▹ bc.1, p ▹D bc.2⟩ := + definition transport_eq (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 (eq.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_eq_deg {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b) - : p ▹ bc ≈ ⟨bc.1, p ▹ bc.2⟩ := + definition transport_eq_deg {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 (eq.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. -/ - definition transport_eq_4deg {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⟩ := + definition transport_eq_4deg {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 revert bcd, - apply (path.rec_on p), intro bcd, + apply (eq.rec_on p), intro bcd, apply (destruct bcd), intros (b, cd), apply (destruct cd), intros (c, d), apply idp @@ -251,24 +251,24 @@ namespace sigma apply (sigma.path (retr f a')), -- "rewrite retr (g (f⁻¹ a'))" apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))), - show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') ≈ b', + show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') = b', from transport_pV B' (retr f a') b' end begin intro u, apply (destruct u), intros (a, b), apply (sigma.path (sect f a)), - show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) ≈ b, + show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) = b, from calc transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) - ≈ g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b))) + = g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b))) : ap_transport (sect f a) (λ a, g a⁻¹) - ... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b))) + ... = g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b))) : ap (g a⁻¹) !transport_compose - ... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b))) + ... = g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b))) : ap (λ x, g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (x⁻¹) (g a b)))) (adj f a) - ... ≈ g a⁻¹ (g a b) : transport_pV - ... ≈ b : sect (g a) b + ... = g a⁻¹ (g a b) : transport_pV + ... = b : sect (g a) b end -- -- "rewrite ap_transport" -- apply concat, apply inverse, apply (ap_transport (sect f a) (λ a, g a⁻¹)), @@ -293,20 +293,20 @@ namespace sigma definition equiv_functor_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a := equiv_functor equiv.refl Hg - definition ap_functor_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b') + definition ap_functor_sigma_dpair (p : a = a') (q : p ▹ b = b') : ap (sigma.functor f g) (sigma.path p q) - ≈ sigma.path (ap f p) + = sigma.path (ap f p) (transport_compose _ f p (g a b)⁻¹ ⬝ ap_transport p g b⁻¹ ⬝ ap (g a') q) := begin reverts (b', q), - apply (path.rec_on p), - intros (b', q), apply (path.rec_on q), + apply (eq.rec_on p), + intros (b', q), apply (eq.rec_on q), apply idp end - definition ap_functor_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) + definition ap_functor_sigma (p : u.1 = v.1) (q : p ▹ u.2 = v.2) : ap (sigma.functor f g) (sigma.path p q) - ≈ sigma.path (ap f p) + = sigma.path (ap f p) (transport_compose B' f p (g u.1 u.2)⁻¹ ⬝ ap_transport p g u.2⁻¹ ⬝ ap (g v.1) q) := begin reverts (p, q), @@ -429,14 +429,14 @@ namespace sigma /- ** Subtypes (sigma types whose second components are hprops) -/ /- To prove equality in a subtype, we only need equality of the first component. -/ - definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 ≈ v.1 → u ≈ v := + definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 = v.1 → u = v := (sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc)))) definition is_equiv_path_hprop [instance] [H : Πa, is_hprop (B a)] (u v : Σa, B a) : is_equiv (path_hprop u v) := !is_equiv.compose - definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 ≈ v.1) ≃ (u ≈ v) + definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 = v.1) ≃ (u = v) := equiv.mk !path_hprop _ @@ -458,7 +458,7 @@ namespace sigma apply IH, apply succ_is_trunc, assumption, intro p, - show is_trunc n (p ▹ u .2 ≈ v .2), from + show is_trunc n (p ▹ u .2 = v .2), from succ_is_trunc n (p ▹ u.2) (v.2), end