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

refactor(hott): use same name convention for sigma in the HoTT and standard libraries

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 18:46:06 -08:00
parent 1e2fc54f2f
commit 2521dbb39e
12 changed files with 56 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
hott/algebra/precategory/constructions.hlean
View file

@ -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

4
hott/algebra/precategory/iso.hlean
View file

@ -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

28
hott/init/axioms/funext_from_ua.hlean
View file

@ -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
)

16
hott/init/axioms/funext_varieties.hlean
View file

@ -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 :=

2
hott/init/hedberg.hlean
View file

@ -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

2
hott/init/trunc.hlean
View file

@ -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

16
hott/init/types/sigma.hlean
View file

@ -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

2
hott/pointed.hlean
View file

@ -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) :=

2
hott/types/pi.hlean
View file

@ -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)) -/

24
hott/types/sigma.hlean
View file

@ -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) :=

4
tests/lean/hott/329.hlean
View file

@ -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

4
tests/lean/hott/sig_noc.hlean
View file

@ -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₂}