From e51ba09a27974a88e1467a511745b22448d9f8b2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 6 Aug 2015 22:37:52 +0200 Subject: [PATCH] feat(hott): add types.sum, greatly expand types.prod, minor changes in types.sigma and types.pi --- hott/book.md | 4 +- hott/init/trunc.hlean | 17 +++- hott/init/types.hlean | 2 +- hott/types/bool.hlean | 7 +- hott/types/fiber.hlean | 4 +- hott/types/nat/hott.hlean | 30 +++---- hott/types/pi.hlean | 2 + hott/types/prod.hlean | 156 ++++++++++++++++++++++++++++++++++++- hott/types/sigma.hlean | 22 ++---- hott/types/sum.hlean | 159 ++++++++++++++++++++++++++++++++++++++ hott/types/types.md | 1 + library/init/prod.lean | 5 +- 12 files changed, 361 insertions(+), 48 deletions(-) create mode 100644 hott/types/sum.hlean diff --git a/hott/book.md b/hott/book.md index 1bafddc21..5a0d693a8 100644 --- a/hott/book.md +++ b/hott/book.md @@ -16,7 +16,7 @@ The rows indicate the chapters, the columns the sections. | | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----| | Ch 1 | . | . | . | . | + | + | + | + | + | . | + | + | | | | -| Ch 2 | + | + | + | + | . | + | + | + | + | + | + | - | + | + | + | +| Ch 2 | + | + | + | + | . | + | + | + | + | + | + | + | + | + | + | | Ch 3 | + | - | + | + | ½ | + | + | - | ½ | . | + | | | | | | Ch 4 | - | + | - | + | . | + | - | - | + | | | | | | | | Ch 5 | - | . | - | - | - | . | . | ½ | | | | | | | | @@ -61,7 +61,7 @@ Chapter 2: Homotopy type theory - 2.9 (Π-types and the function extensionality axiom): [init.funext](init/funext.hlean) and [types.pi](types/pi.hlean) - 2.10 (Universes and the univalence axiom): [init.ua](init/ua.hlean) - 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [types.cubical.square](types/cubical/square.hlean) (characterization of pathovers in equality types) -- 2.12 (Coproducts): not formalized +- 2.12 (Coproducts): [types.sum](types/sum.hlean) - 2.13 (Natural numbers): [types.nat.hott](types/nat/hott.hlean) - 2.14 (Example: equality of structures): algebra formalized in [algebra.group](algebra/group.hlean). - 2.15 (Universal properties): in the corresponding file in the [types](types/types.md) folder. diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 68fcd3a1b..31c4fcdf8 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -189,12 +189,20 @@ namespace is_trunc : is_contr (Σ(x : A), a = x) := is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp)) - definition is_contr_unit [instance] : is_contr unit := + definition is_contr_unit : is_contr unit := is_contr.mk star (λp, unit.rec_on p idp) - definition is_hprop_empty [instance] : is_hprop empty := + definition is_hprop_empty : is_hprop empty := is_hprop.mk (λx, !empty.elim x) + local attribute is_contr_unit is_hprop_empty [instance] + + definition is_trunc_unit [instance] (n : trunc_index) : is_trunc n unit := + !is_trunc_of_is_contr + + definition is_trunc_empty [instance] (n : trunc_index) : is_trunc (n.+1) empty := + !is_trunc_succ_of_is_hprop + /- truncated universe -/ -- TODO: move to root namespace? @@ -292,6 +300,11 @@ namespace is_trunc theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' := !is_hprop.elim + /- truncatedness of lift -/ + definition is_trunc_lift [instance] (A : Type) (n : trunc_index) [H : is_trunc n A] + : is_trunc n (lift A) := + is_trunc_equiv_closed _ !equiv_lift + -- TODO: port "Truncated morphisms" end is_trunc diff --git a/hott/init/types.hlean b/hott/init/types.hlean index 260ab1212..c173c5271 100644 --- a/hott/init/types.hlean +++ b/hott/init/types.hlean @@ -85,7 +85,7 @@ namespace prod infixr × := prod namespace ops - infixr * := prod + infixr [parsing-only] * := prod postfix `.1`:(max+1) := pr1 postfix `.2`:(max+1) := pr2 abbreviation pr₁ := @pr1 diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean index 7915d96eb..5b8f7d466 100644 --- a/hott/types/bool.hlean +++ b/hott/types/bool.hlean @@ -17,11 +17,8 @@ namespace bool begin fapply is_equiv.mk, exact bnot, - do 3 focus (intro b;cases b;all_goals (exact idp)) - --should information be propagated with all_goals? - -- all_goals (intro b;cases b), - -- all_goals (exact idp) --- all_goals (focus (intro b;cases b;all_goals (exact idp))), + all_goals (intro b;cases b), do 6 reflexivity +-- all_goals (focus (intro b;cases b;all_goals reflexivity)), end definition equiv_bnot : bool ≃ bool := equiv.mk bnot _ diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 18e4ea142..3ae3efdcd 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -31,9 +31,9 @@ namespace fiber : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) := begin apply equiv.trans, - {apply eq_equiv_fn_eq_of_equiv, apply sigma_char}, + apply eq_equiv_fn_eq_of_equiv, apply sigma_char, apply equiv.trans, - {apply equiv.symm, apply equiv_sigma_eq}, + apply sigma_eq_equiv, apply sigma_equiv_sigma_id, intro p, apply pathover_eq_equiv_Fl, diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index b7e1e3bad..eb21ad184 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -77,38 +77,38 @@ namespace nat exfalso, apply lt.irrefl, apply lt_of_le_of_lt H H'} end - definition code [reducible] [unfold 1 2] : ℕ → ℕ → Type₀ - | code 0 0 := unit + protected definition code [reducible] [unfold 1 2] : ℕ → ℕ → Type₀ + | code 0 0 := unit + | code 0 (succ m) := empty | code (succ n) 0 := empty - | code 0 (succ m) := empty | code (succ n) (succ m) := code n m - definition refl : Πn, code n n - | refl 0 := star + protected definition refl : Πn, nat.code n n + | refl 0 := star | refl (succ n) := refl n - definition encode [unfold 3] {n m : ℕ} (p : n = m) : code n m := - p ▸ refl n + protected definition encode [unfold 3] {n m : ℕ} (p : n = m) : nat.code n m := + p ▸ nat.refl n - definition decode : Π(n m : ℕ), code n m → n = m - | decode 0 0 := λc, idp - | decode 0 (succ l) := λc, empty.elim c _ + protected definition decode : Π(n m : ℕ), nat.code n m → n = m + | decode 0 0 := λc, idp + | decode 0 (succ l) := λc, empty.elim c _ | decode (succ k) 0 := λc, empty.elim c _ | decode (succ k) (succ l) := λc, ap succ (decode k l c) - definition nat_eq_equiv (n m : ℕ) : (n = m) ≃ code n m := - equiv.MK encode - !decode + definition nat_eq_equiv (n m : ℕ) : (n = m) ≃ nat.code n m := + equiv.MK nat.encode + !nat.decode begin revert m, induction n, all_goals (intro m;induction m;all_goals intro c), all_goals try contradiction, induction c, reflexivity, - xrewrite [↑decode,-tr_compose,v_0], + xrewrite [↑nat.decode,-tr_compose,v_0], end begin intro p, induction p, esimp, induction n, reflexivity, - rewrite [↑decode,↑refl,v_0] + rewrite [↑nat.decode,↑nat.refl,v_0] end end nat diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index a5acee324..a3841426d 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -45,6 +45,8 @@ namespace pi definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ~ g) := equiv.mk apd10 _ + definition pi_eq_equiv (f g : Πx, B x) : (f = g) ≃ (f ~ g) := !eq_equiv_homotopy + definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) := _ diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index b28a3b6aa..7d6cb4444 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -7,7 +7,7 @@ Ported from Coq HoTT Theorems about products -/ -open eq equiv is_equiv is_trunc prod prod.ops unit +open eq equiv is_equiv is_trunc prod prod.ops unit equiv.ops variables {A A' B B' C D : Type} {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B} @@ -17,12 +17,106 @@ namespace prod protected definition eta (u : A × B) : (pr₁ u, pr₂ u) = u := by cases u; apply idp - definition pair_eq (pa : a = a') (pb : b = b') : (a, b) = (a', b') := + definition pair_eq [unfold 7 8] (pa : a = a') (pb : b = b') : (a, b) = (a', b') := by cases pa; cases pb; apply idp - definition prod_eq (H₁ : pr₁ u = pr₁ v) (H₂ : pr₂ u = pr₂ v) : u = v := + definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v := by cases u; cases v; exact pair_eq H₁ H₂ + /- Projections of paths from a total space -/ + + definition eq_pr1 (p : u = v) : u.1 = v.1 := + ap pr1 p + + definition eq_pr2 (p : u = v) : u.2 = v.2 := + ap pr2 p + + namespace ops + postfix `..1`:(max+1) := eq_pr1 + postfix `..2`:(max+1) := eq_pr2 + end ops + open ops + + definition pair_prod_eq (p : u.1 = v.1) (q : u.2 = v.2) + : ((prod_eq p q)..1, (prod_eq p q)..2) = (p, q) := + by induction u; induction v;esimp at *;induction p;induction q;reflexivity + + definition prod_eq_pr1 (p : u.1 = v.1) (q : u.2 = v.2) : (prod_eq p q)..1 = p := + (pair_prod_eq p q)..1 + + definition prod_eq_pr2 (p : u.1 = v.1) (q : u.2 = v.2) : (prod_eq p q)..2 = q := + (pair_prod_eq p q)..2 + + definition prod_eq_eta (p : u = v) : prod_eq (p..1) (p..2) = p := + by induction p; induction u; reflexivity + + /- the uncurried version of prod_eq. We will prove that this is an equivalence -/ + + definition prod_eq_unc (H : u.1 = v.1 × u.2 = v.2) : u = v := + by cases H with H₁ H₂;exact prod_eq H₁ H₂ + + definition pair_prod_eq_unc : Π(pq : u.1 = v.1 × u.2 = v.2), + ((prod_eq_unc pq)..1, (prod_eq_unc pq)..2) = pq + | pair_prod_eq_unc (pq₁, pq₂) := pair_prod_eq pq₁ pq₂ + + definition prod_eq_unc_pr1 (pq : u.1 = v.1 × u.2 = v.2) : (prod_eq_unc pq)..1 = pq.1 := + (pair_prod_eq_unc pq)..1 + + definition prod_eq_unc_pr2 (pq : u.1 = v.1 × u.2 = v.2) : (prod_eq_unc pq)..2 = pq.2 := + (pair_prod_eq_unc pq)..2 + + definition prod_eq_unc_eta (p : u = v) : prod_eq_unc (p..1, p..2) = p := + prod_eq_eta p + + definition is_equiv_prod_eq [instance] (u v : A × B) + : is_equiv (prod_eq_unc : u.1 = v.1 × u.2 = v.2 → u = v) := + adjointify prod_eq_unc + (λp, (p..1, p..2)) + prod_eq_unc_eta + pair_prod_eq_unc + + definition prod_eq_equiv (u v : A × B) : (u = v) ≃ (u.1 = v.1 × u.2 = v.2) := + (equiv.mk prod_eq_unc _)⁻¹ᵉ + + /- Transport -/ + + definition prod_transport {P Q : A → Type} {a a' : A} (p : a = a') (u : P a × Q a) + : p ▸ u = (p ▸ u.1, p ▸ u.2) := + by induction p; induction u; reflexivity + + /- Functorial action -/ + + variables (f : A → A') (g : B → B') + definition prod_functor [unfold 7] (u : A × B) : A' × B' := + (f u.1, g u.2) + + definition ap_prod_functor (p : u.1 = v.1) (q : u.2 = v.2) + : ap (prod_functor f g) (prod_eq p q) = prod_eq (ap f p) (ap g q) := + by induction u; induction v; esimp at *; induction p; induction q; reflexivity + + /- Equivalences -/ + + definition is_equiv_prod_functor [instance] [H : is_equiv f] [H : is_equiv g] + : is_equiv (prod_functor f g) := + begin + apply adjointify _ (prod_functor f⁻¹ g⁻¹), + intro u, induction u, rewrite [▸*,right_inv f,right_inv g], + intro u, induction u, rewrite [▸*,left_inv f,left_inv g], + end + + definition prod_equiv_prod_of_is_equiv [H : is_equiv f] [H : is_equiv g] + : A × B ≃ A' × B' := + equiv.mk (prod_functor f g) _ + + definition prod_equiv_prod (f : A ≃ A') (g : B ≃ B') : A × B ≃ A' × B' := + equiv.mk (prod_functor f g) _ + + definition prod_equiv_prod_left (g : B ≃ B') : A × B ≃ A × B' := + prod_equiv_prod equiv.refl g + + definition prod_equiv_prod_right (f : A ≃ A') : A × B ≃ A' × B := + prod_equiv_prod f equiv.refl + /- Symmetry -/ definition is_equiv_flip [instance] (A B : Type) : is_equiv (@flip A B) := @@ -34,6 +128,17 @@ namespace prod definition prod_comm_equiv (A B : Type) : A × B ≃ B × A := equiv.mk flip _ + /- Associativity -/ + + definition prod_assoc_equiv (A B C : Type) : A × (B × C) ≃ (A × B) × C := + begin + fapply equiv.MK, + { intro z, induction z with a z, induction z with b c, exact (a, b, c)}, + { intro z, induction z with z c, induction z with a b, exact (a, (b, c))}, + { intro z, induction z with z c, induction z with a b, reflexivity}, + { intro z, induction z with a z, induction z with b c, reflexivity}, + end + definition prod_contr_equiv (A B : Type) [H : is_contr B] : A × B ≃ A := equiv.MK pr1 (λx, (x, !center)) @@ -43,6 +148,49 @@ namespace prod definition prod_unit_equiv (A : Type) : A × unit ≃ A := !prod_contr_equiv - -- is_trunc_prod is defined in sigma + /- Universal mapping properties -/ + definition is_equiv_prod_rec [instance] (P : A × B → Type) + : is_equiv (prod.rec : (Πa b, P (a, b)) → Πu, P u) := + adjointify _ + (λg a b, g (a, b)) + (λg, eq_of_homotopy (λu, by induction u;reflexivity)) + (λf, idp) + + definition equiv_prod_rec (P : A × B → Type) : (Πa b, P (a, b)) ≃ (Πu, P u) := + equiv.mk prod.rec _ + + definition imp_imp_equiv_prod_imp (A B C : Type) : (A → B → C) ≃ (A × B → C) := + !equiv_prod_rec + + definition prod_corec_unc [unfold 4] {P Q : A → Type} (u : (Πa, P a) × (Πa, Q a)) (a : A) + : P a × Q a := + (u.1 a, u.2 a) + + definition is_equiv_prod_corec (P Q : A → Type) + : is_equiv (prod_corec_unc : (Πa, P a) × (Πa, Q a) → Πa, P a × Q a) := + adjointify _ + (λg, (λa, (g a).1, λa, (g a).2)) + (by intro g; apply eq_of_homotopy; intro a; esimp; induction (g a); reflexivity) + (by intro h; induction h with f g; reflexivity) + + definition equiv_prod_corec (P Q : A → Type) : ((Πa, P a) × (Πa, Q a)) ≃ (Πa, P a × Q a) := + equiv.mk _ !is_equiv_prod_corec + + definition imp_prod_imp_equiv_imp_prod (A B C : Type) : (A → B) × (A → C) ≃ (A → (B × C)) := + !equiv_prod_corec + + definition is_trunc_prod (A B : Type) (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B] + : is_trunc n (A × B) := + begin + revert A B HA HB, induction n with n IH, all_goals intro A B HA HB, + { fapply is_contr.mk, + exact (!center, !center), + intro u, apply prod_eq, all_goals apply center_eq}, + { apply is_trunc_succ_intro, intro u v, + apply is_trunc_equiv_closed_rev, apply prod_eq_equiv, + exact IH _ _ _ _} + end end prod + +attribute prod.is_trunc_prod [instance] [priority 1505] diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index f7decb8d3..75cc004c2 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -95,8 +95,8 @@ namespace sigma sigma_eq_eta_unc dpair_sigma_eq_unc - definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1), u.2 =[p] v.2) ≃ (u = v) := - equiv.mk sigma_eq_unc !is_equiv_sigma_eq + definition sigma_eq_equiv (u v : Σa, B a) : (u = v) ≃ (Σ(p : u.1 = v.1), u.2 =[p] v.2) := + (equiv.mk sigma_eq_unc _)⁻¹ᵉ definition dpair_eq_dpair_con (p1 : a = a' ) (q1 : b =[p1] b' ) (p2 : a' = a'') (q2 : b' =[p2] b'') : @@ -157,18 +157,18 @@ 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) + definition sigma_transport (p : a = a') (bc : Σ(b : B a), C a b) : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ := by induction p; induction bc; reflexivity /- The special case when the second variable doesn't depend on the first is simpler. -/ - definition tr_eq_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b) + definition sigma_transport_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b) : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ := by induction p; induction bc; reflexivity /- Or if the second variable contains a first component that doesn't depend on the first. -/ - definition tr_eq2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a') + definition sigma_transport2_nondep {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 induction p, induction bcd with b cd, induction cd, reflexivity @@ -362,17 +362,11 @@ namespace sigma induction n with n IH, { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_pr1}, { intro A B HA HB, apply is_trunc_succ_intro, intro u v, - apply is_trunc_equiv_closed, - apply equiv_sigma_eq, + apply is_trunc_equiv_closed_rev, + apply sigma_eq_equiv, exact IH _ _ _ _} end end sigma -attribute sigma.is_trunc_sigma [instance] [priority 1505] - -open is_trunc sigma prod -/- truncatedness -/ -definition prod.is_trunc_prod [instance] [priority 1490] (A B : Type) (n : trunc_index) - [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) := -is_trunc.is_trunc_equiv_closed n !equiv_prod +attribute sigma.is_trunc_sigma [instance] [priority 1490] diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean new file mode 100644 index 000000000..f35f21793 --- /dev/null +++ b/hott/types/sum.hlean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2015 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Floris van Doorn + +Theorems about sums/coproducts/disjoint unions +-/ + +open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool + +namespace sum + universe variables u v + variables {A : Type.{u}} {B : Type.{v}} (z z' : A + B) + + protected definition eta : sum.rec inl inr z = z := + by induction z; all_goals reflexivity + + protected definition code [unfold 3 4] : A + B → A + B → Type.{max u v} + | code (inl a) (inl a') := lift.{u v} (a = a') + | code (inr b) (inr b') := lift.{v u} (b = b') + | code _ _ := lift empty + + protected definition decode [unfold 3 4] : Π(z z' : A + B), sum.code z z' → z = z' + | decode (inl a) (inl a') := λc, ap inl (down c) + | decode (inl a) (inr b') := λc, empty.elim (down c) _ + | decode (inr b) (inl a') := λc, empty.elim (down c) _ + | decode (inr b) (inr b') := λc, ap inr (down c) + + variables {z z'} + protected definition encode [unfold 3 4 5] (p : z = z') : sum.code z z' := + by induction p; induction z; all_goals exact up idp + + variables (z z') + definition sum_eq_equiv : (z = z') ≃ sum.code z z' := + equiv.MK sum.encode + !sum.decode + abstract begin + intro c, induction z with a b, all_goals induction z' with a' b', + all_goals (esimp at *; induction c with c), + all_goals induction c, -- c either has type empty or a path + all_goals reflexivity + end end + abstract begin + intro p, induction p, induction z, all_goals reflexivity + end end + + section + variables {a a' : A} {b b' : B} + definition eq_of_inl_eq_inl [unfold 5] (p : inl a = inl a' :> A + B) : a = a' := + down (sum.encode p) + definition eq_of_inr_eq_inr [unfold 5] (p : inr b = inr b' :> A + B) : b = b' := + down (sum.encode p) + definition empty_of_inl_eq_inr (p : inl a = inr b) : empty := down (sum.encode p) + definition empty_of_inr_eq_inl (p : inr b = inl a) : empty := down (sum.encode p) + + definition sum_transport {P Q : A → Type} (p : a = a') (z : P a + Q a) + : p ▸ z = sum.rec (λa, inl (p ▸ a)) (λb, inr (p ▸ b)) z := + by induction p; induction z; all_goals reflexivity + end + + variables {A' B' : Type} (f : A → A') (g : B → B') + definition sum_functor [unfold 7] : A + B → A' + B' + | sum_functor (inl a) := inl (f a) + | sum_functor (inr b) := inr (g b) + + definition is_equiv_sum_functor [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (sum_functor f g) := + adjointify (sum_functor f g) + (sum_functor f⁻¹ g⁻¹) + abstract begin + intro z, induction z, + all_goals (esimp; (apply ap inl | apply ap inr); apply right_inv) + end end + abstract begin + intro z, induction z, + all_goals (esimp; (apply ap inl | apply ap inr); apply right_inv) + end end + + definition sum_equiv_sum_of_is_equiv [Hf : is_equiv f] [Hg : is_equiv g] : A + B ≃ A' + B' := + equiv.mk _ (is_equiv_sum_functor f g) + + definition sum_equiv_sum (f : A ≃ A') (g : B ≃ B') : A + B ≃ A' + B' := + equiv.mk _ (is_equiv_sum_functor f g) + + definition sum_equiv_sum_left (g : B ≃ B') : A + B ≃ A + B' := + sum_equiv_sum equiv.refl g + + definition sum_equiv_sum_right (f : A ≃ A') : A + B ≃ A' + B := + sum_equiv_sum f equiv.refl + + definition flip : A + B → B + A + | flip (inl a) := inr a + | flip (inr b) := inl b + + definition sum_comm_equiv (A B : Type) : A + B ≃ B + A := + begin + fapply equiv.MK, + exact flip, + exact flip, + all_goals (intro z; induction z; all_goals reflexivity) + end + + -- definition sum_assoc_equiv (A B C : Type) : A + (B + C) ≃ (A + B) + C := + -- begin + -- fapply equiv.MK, + -- all_goals try (intro z; induction z with u v; + -- all_goals try induction u; all_goals try induction v), + -- all_goals try (repeat (apply inl | apply inr | assumption); now), + -- end + + definition sum_empty_equiv (A : Type) : A + empty ≃ A := + begin + fapply equiv.MK, + intro z, induction z, assumption, contradiction, + exact inl, + intro a, reflexivity, + intro z, induction z, reflexivity, contradiction + end + + definition sum_rec_unc {P : A + B → Type} (fg : (Πa, P (inl a)) × (Πb, P (inr b))) : Πz, P z := + sum.rec fg.1 fg.2 + + definition is_equiv_sum_rec (P : A + B → Type) + : is_equiv (sum_rec_unc : (Πa, P (inl a)) × (Πb, P (inr b)) → Πz, P z) := + begin + apply adjointify sum_rec_unc (λf, (λa, f (inl a), λb, f (inr b))), + intro f, apply eq_of_homotopy, intro z, focus (induction z; all_goals reflexivity), + intro h, induction h with f g, reflexivity + end + + definition equiv_sum_rec (P : A + B → Type) : (Πa, P (inl a)) × (Πb, P (inr b)) ≃ Πz, P z := + equiv.mk _ !is_equiv_sum_rec + + definition imp_prod_imp_equiv_sum_imp (A B C : Type) : (A → C) × (B → C) ≃ (A + B → C) := + !equiv_sum_rec + + definition is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A] [HB : is_trunc (n.+2) B] + : is_trunc (n.+2) (A + B) := + begin + apply is_trunc_succ_intro, intro z z', + apply is_trunc_equiv_closed_rev, apply sum_eq_equiv, + induction z with a b, all_goals induction z' with a' b', all_goals esimp, + all_goals exact _, + end + + /- Sums are equivalent to dependent sigmas where the first component is a bool. -/ + + definition sum_of_sigma_bool {A B : Type} (v : Σ(b : bool), bool.rec A B b) : A + B := + by induction v with b x; induction b; exact inl x; exact inr x + + definition sigma_bool_of_sum {A B : Type} (z : A + B) : Σ(b : bool), bool.rec A B b := + by induction z with a b; exact ⟨ff, a⟩; exact ⟨tt, b⟩ + + definition sum_equiv_sigma_bool (A B : Type) : A + B ≃ Σ(b : bool), bool.rec A B b := + equiv.MK sigma_bool_of_sum + sum_of_sigma_bool + begin intro v, induction v with b x, induction b, all_goals reflexivity end + begin intro z, induction z with a b, all_goals reflexivity end + +end sum diff --git a/hott/types/types.md b/hott/types/types.md index a60451f33..e5a5c8886 100644 --- a/hott/types/types.md +++ b/hott/types/types.md @@ -9,6 +9,7 @@ Types (not necessarily HoTT-related): * [int](int/int.md) (subfolder) * [prod](prod.hlean) * [sigma](sigma.hlean) +* [sum](sum.hlean) * [pi](pi.hlean) * [arrow](arrow.hlean) * [W](W.hlean): W-types (not loaded by default) diff --git a/library/init/prod.lean b/library/init/prod.lean index a2a95c965..b2b0d2039 100644 --- a/library/init/prod.lean +++ b/library/init/prod.lean @@ -12,10 +12,9 @@ notation A × B := prod A B notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t namespace prod - notation A * B := prod A B - notation A × B := prod A B -- repeat, so this takes precedence + notation [parsing-only] A * B := prod A B namespace low_precedence_times - reserve infixr `*`:30 -- conflicts with notation for multiplication + reserve infixr [parsing-only] `*`:30 -- conflicts with notation for multiplication infixr `*` := prod end low_precedence_times