From 2521dbb39ed62e4bab7983eeaabfd0ed4b2992e0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Dec 2014 18:46:06 -0800 Subject: [PATCH] refactor(hott): use same name convention for sigma in the HoTT and standard libraries --- hott/algebra/precategory/constructions.hlean | 10 +++---- hott/algebra/precategory/iso.hlean | 4 +-- hott/init/axioms/funext_from_ua.hlean | 28 ++++++++++---------- hott/init/axioms/funext_varieties.hlean | 16 +++++------ hott/init/hedberg.hlean | 2 +- hott/init/trunc.hlean | 2 +- hott/init/types/sigma.hlean | 16 +++++------ hott/pointed.hlean | 2 +- hott/types/pi.hlean | 2 +- hott/types/sigma.hlean | 24 ++++++++--------- tests/lean/hott/329.hlean | 4 +-- tests/lean/hott/sig_noc.hlean | 4 +-- 12 files changed, 56 insertions(+), 58 deletions(-) diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean index ec2e4eece..30671e9fc 100644 --- a/hott/algebra/precategory/constructions.hlean +++ b/hott/algebra/precategory/constructions.hlean @@ -168,9 +168,9 @@ namespace precategory variables {ob : Type} {C : precategory ob} {c : ob} protected definition slice_obs (C : precategory ob) (c : ob) := Σ(b : ob), hom b c variables {a b : slice_obs C c} - protected definition to_ob (a : slice_obs C c) : ob := dpr1 a - protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl - protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a + protected definition to_ob (a : slice_obs C c) : ob := pr1 a + protected definition to_ob_def (a : slice_obs C c) : to_ob a = pr1 a := rfl + protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := pr2 a -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b) -- (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b := -- sigma.equal H₁ H₂ @@ -179,8 +179,8 @@ namespace precategory protected definition slice_hom (a b : slice_obs C c) : Type := Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a - protected definition hom_hom (f : slice_hom a b) : hom (to_ob a) (to_ob b) := dpr1 f - protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := dpr2 f + protected definition hom_hom (f : slice_hom a b) : hom (to_ob a) (to_ob b) := pr1 f + protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := pr2 f -- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g := -- sigma.equal H !proof_irrel diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean index 8ed2205ea..d9ad03a84 100644 --- a/hott/algebra/precategory/iso.hlean +++ b/hott/algebra/precategory/iso.hlean @@ -21,7 +21,7 @@ namespace morphism exact (pr₂ S.2), fapply adjointify, intro H, apply (is_iso.rec_on H), intros (g, η, ε), - exact (dpair g (pair η ε)), + exact (sigma.mk g (pair η ε)), intro H, apply (is_iso.rec_on H), intros (g, η, ε), apply idp, intro S, apply (sigma.rec_on S), intros (g, ηε), apply (prod.rec_on ηε), intros (η, ε), apply idp, @@ -35,7 +35,7 @@ namespace morphism intro S, apply isomorphic.mk, apply (S.2), fapply adjointify, intro p, apply (isomorphic.rec_on p), intros (f, H), - exact (dpair f H), + exact (sigma.mk f H), intro p, apply (isomorphic.rec_on p), intros (f, H), apply idp, intro S, apply (sigma.rec_on S), intros (f, H), apply idp, end diff --git a/hott/init/axioms/funext_from_ua.hlean b/hott/init/axioms/funext_from_ua.hlean index 89a9fddac..b48c2ae15 100644 --- a/hott/init/axioms/funext_from_ua.hlean +++ b/hott/init/axioms/funext_from_ua.hlean @@ -59,10 +59,10 @@ context protected definition isequiv_src_compose {A B : Type} : @is_equiv (A → diagonal B) (A → B) - (compose (pr₁ ∘ dpr1)) := - @ua_isequiv_postcompose _ _ _ (pr₁ ∘ dpr1) - (is_equiv.adjointify (pr₁ ∘ dpr1) - (λ x, dpair (x , x) idp) (λx, idp) + (compose (pr₁ ∘ pr1)) := + @ua_isequiv_postcompose _ _ _ (pr₁ ∘ pr1) + (is_equiv.adjointify (pr₁ ∘ pr1) + (λ x, sigma.mk (x , x) idp) (λx, idp) (λ x, sigma.rec_on x (λ xy, prod.rec_on xy (λ b c p, eq.rec_on p idp)))) @@ -70,10 +70,10 @@ context protected definition isequiv_tgt_compose {A B : Type} : @is_equiv (A → diagonal B) (A → B) - (compose (pr₂ ∘ dpr1)) := - @ua_isequiv_postcompose _ _ _ (pr2 ∘ dpr1) - (is_equiv.adjointify (pr2 ∘ dpr1) - (λ x, dpair (x , x) idp) (λx, idp) + (compose (pr₂ ∘ pr1)) := + @ua_isequiv_postcompose _ _ _ (pr2 ∘ pr1) + (is_equiv.adjointify (pr2 ∘ pr1) + (λ x, sigma.mk (x , x) idp) (λx, idp) (λ x, sigma.rec_on x (λ xy, prod.rec_on xy (λ b c p, eq.rec_on p idp)))) @@ -81,21 +81,21 @@ context theorem nondep_funext_from_ua {A : Type} {B : Type.{l+1}} : Π {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 - let precomp1 := compose (pr₁ ∘ dpr1) in + let d := λ (x : A), sigma.mk (f x , f x) idp in + let e := λ (x : A), sigma.mk (f x , g x) (p x) in + let precomp1 := compose (pr₁ ∘ pr1) in have equiv1 [visible] : is_equiv precomp1, from @isequiv_src_compose A B, 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₁ ∘ pr1 ∘ x = pr₁ ∘ pr1 ∘ y → x = y, from (λ x y, is_equiv.inv (ap precomp1)), - have eq2 : pr₁ ∘ dpr1 ∘ d = pr₁ ∘ dpr1 ∘ e, + have eq2 : pr₁ ∘ pr1 ∘ d = pr₁ ∘ pr1 ∘ e, from idp, have eq0 : d = e, from H' d e eq2, - have eq1 : (pr₂ ∘ dpr1) ∘ d = (pr₂ ∘ dpr1) ∘ e, + have eq1 : (pr₂ ∘ pr1) ∘ d = (pr₂ ∘ pr1) ∘ e, from ap _ eq0, eq1 ) diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index 227d9cfb6..4523003ca 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -58,22 +58,22 @@ context protected definition idhtpy : f ∼ f := (λ x, idp) definition contr_basedhtpy [instance] : is_contr (Σ (g : Π x, B x), f ∼ g) := - is_contr.mk (dpair f idhtpy) + is_contr.mk (sigma.mk f idhtpy) (λ dp, sigma.rec_on dp (λ (g : Π x, B x) (h : f ∼ g), 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 + @sigma.mk _ (λg, f ∼ g) + (λx, pr1 (k x)) (λx, pr2 (k x)) in + let s := λ g h x, @sigma.mk _ (λy, f x = y) (g x) (h x) in have t1 : Πx, is_contr (Σ y, f x = y), from (λx, !contr_basedpaths), 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, + have t3 : (λ x, @sigma.mk _ (λ 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 t4 : r (λ x, sigma.mk (f x) idp) = r (s g h), from ap r t3, - have endt : dpair f idhtpy = dpair g h, + have endt : sigma.mk f idhtpy = sigma.mk g h, from t4, endt ) @@ -82,7 +82,7 @@ context parameters (Q : Π g (h : f ∼ g), Type) (d : Q f idhtpy) definition htpy_ind (g : Πx, B x) (h : f ∼ g) : Q g h := - @transport _ (λ gh, Q (dpr1 gh) (dpr2 gh)) (dpair f idhtpy) (dpair g h) + @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h) (@path_contr _ contr_basedhtpy _ _) d definition htpy_ind_beta : htpy_ind f idhtpy = d := diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean index f6832e8f5..bd2dab47b 100644 --- a/hott/init/hedberg.hlean +++ b/hott/init/hedberg.hlean @@ -8,7 +8,7 @@ Hedberg's Theorem: every type with decidable equality is a hset -/ prelude import init.nat init.trunc -open eq eq.ops nat truncation sigma.ops +open eq eq.ops nat truncation sigma -- TODO(Leo): move const coll and path_coll to a different file? private definition const {A B : Type} (f : A → B) := ∀ x y, f x = f y diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index c4093033d..22e6c6261 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -176,7 +176,7 @@ namespace truncation /- 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, eq.rec_on q idp)) + is_contr.mk (sigma.mk 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 diff --git a/hott/init/types/sigma.hlean b/hott/init/types/sigma.hlean index ce2324acd..316bb4d5e 100644 --- a/hott/init/types/sigma.hlean +++ b/hott/init/types/sigma.hlean @@ -4,22 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ prelude -import ..num ..wf ..logic ..tactic +import init.num structure sigma {A : Type} (B : A → Type) := -dpair :: (dpr1 : A) (dpr2 : B dpr1) +mk :: (pr1 : A) (pr2 : B pr1) notation `Σ` binders `,` r:(scoped P, sigma P) := r namespace sigma - - notation `dpr₁` := dpr1 - notation `dpr₂` := dpr2 + notation `pr₁` := pr1 + notation `pr₂` := pr2 + notation `⟨`:max t:(foldr `,` (e r, mk e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \> namespace ops - postfix `.1`:(max+1) := dpr1 - postfix `.2`:(max+1) := dpr2 - notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \> + postfix `.1`:(max+1) := pr1 + postfix `.2`:(max+1) := pr2 end ops - end sigma diff --git a/hott/pointed.hlean b/hott/pointed.hlean index 7682c1833..8c0c0818d 100644 --- a/hott/pointed.hlean +++ b/hott/pointed.hlean @@ -23,7 +23,7 @@ namespace is_pointed -- A sigma type of pointed components is pointed protected definition sigma [instance] {P : A → Type} [G : is_pointed A] [H : is_pointed (P (point A))] : is_pointed (Σx, P x) := - is_pointed.mk (sigma.dpair (point A) (point (P (point A)))) + is_pointed.mk (sigma.mk (point A) (point (P (point A)))) protected definition prod [H1 : is_pointed A] [H2 : is_pointed B] : is_pointed (A × B) := diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 6f620ade1..67a8840da 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -79,7 +79,7 @@ namespace pi : (Π(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 + section open sigma sigma.ops /- more implicit arguments: (Π(b : B a), eq.transport C (sigma.path p idp) (f b) = g (p ▹ b)) ≃ (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) = g (eq.transport B p b)) -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 97ac35323..ef55e1da6 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -26,7 +26,7 @@ namespace sigma 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' := + definition dpair_eq_dpair (p : a = a') (q : p ▹ b = b') : sigma.mk a b = sigma.mk 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 -/ @@ -38,7 +38,7 @@ namespace sigma /- Projections of paths from a total space -/ definition path_pr1 (p : u = v) : u.1 = v.1 := - ap dpr1 p + ap pr1 p postfix `..1`:(max+1) := path_pr1 @@ -50,7 +50,7 @@ namespace sigma 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⟩ := + : sigma.mk (sigma.path p q)..1 (sigma.path p q)..2 = ⟨p, q⟩ := begin reverts (p, q), apply (destruct u), intros (u1, u2), @@ -85,11 +85,11 @@ namespace sigma /- 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 : pr1 u = pr1 v), p ▹ (pr2 u) = pr2 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 := + : sigma.mk (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) @@ -100,7 +100,7 @@ namespace sigma : (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 (sigma.mk p..1 p..2) = p := !sigma_path_eta definition transport_sigma_path_dpr1_uncurried {B' : A → Type} @@ -158,7 +158,7 @@ namespace sigma /- 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 := + definition ap_dpair (q : b₁ = b₂) : ap (sigma.mk a) q = dpair_eq_dpair idp q := eq.rec_on q idp /- Dependent transport is the same as transport along a sigma_eq. -/ @@ -318,14 +318,14 @@ namespace sigma /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/ open truncation definition is_equiv_dpr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)] - : is_equiv (@dpr1 A B) := - adjointify dpr1 + : is_equiv (@pr1 A B) := + adjointify pr1 (λa, ⟨a, !center⟩) (λa, idp) (λu, sigma.path idp !contr) definition equiv_of_all_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A := - equiv.mk dpr1 _ + equiv.mk pr1 _ /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/ @@ -375,7 +375,7 @@ namespace sigma ... ≃ (Σa' a, C (a, a')) : assoc_equiv_prod definition symm_equiv (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') := - symm_equiv_uncurried (λu, C (pr1 u) (pr2 u)) + symm_equiv_uncurried (λu, C (prod.pr1 u) (prod.pr2 u)) definition equiv_prod (A B : Type) : (Σ(a : A), B) ≃ A × B := equiv.mk _ (adjointify @@ -430,7 +430,7 @@ namespace sigma /- 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 := - (sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc)))) + (sigma_path_uncurried ∘ (@inv _ _ pr1 (@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) := diff --git a/tests/lean/hott/329.hlean b/tests/lean/hott/329.hlean index e50722551..f338639f1 100644 --- a/tests/lean/hott/329.hlean +++ b/tests/lean/hott/329.hlean @@ -3,10 +3,10 @@ open eq sigma variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a} -definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : dpair a b = dpair a' b' := +definition path_sigma_dpair (p : a = a') (q : p ▹ b = b') : sigma.mk a b = sigma.mk a' b' := eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q -definition path_sigma (p : dpr1 u = dpr1 v) (q : p ▹ dpr2 u = dpr2 v) : u = v := +definition path_sigma (p : pr1 u = pr1 v) (q : p ▹ pr2 u = pr2 v) : u = v := destruct u (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair)) p q diff --git a/tests/lean/hott/sig_noc.hlean b/tests/lean/hott/sig_noc.hlean index f60cf7b31..e30ff7baa 100644 --- a/tests/lean/hott/sig_noc.hlean +++ b/tests/lean/hott/sig_noc.hlean @@ -1,6 +1,6 @@ namespace sigma open lift - open sigma.ops + open sigma.ops sigma variables {A : Type} {B : A → Type} variables {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} @@ -22,7 +22,7 @@ mk :: (A : Type) (B : A → Type) (a : A) (b : B a) set_option pp.implicit true namespace foo - open lift sigma.ops + open lift sigma sigma.ops universe variables l₁ l₂ variables {A₁ : Type.{l₁}} {B₁ : A₁ → Type.{l₂}} {a₁ : A₁} {b₁ : B₁ a₁} variables {A₂ : Type.{l₁}} {B₂ : A₂ → Type.{l₂}} {a₂ : A₂} {b₂ : B₂ a₂}