Permalink
Switch branches/tags
Nothing to show
Find file Copy path
c534985 Sep 11, 2018
2 contributors

Users who have contributed to this file

@fpvandoorn @leodemoura
475 lines (390 sloc) 19 KB
/-
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
-/
import .pi .equiv logic
open lift eq is_equiv equiv prod prod.ops is_trunc sigma bool
namespace sum
universe variables u v u' v'
variables {A : Type.{u}} {B : Type.{v}} (z z' : A + B) {P : A Type.{u'}} {Q : A Type.{v'}}
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 (a = a')
| code (inr b) (inr b') := lift (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)
protected definition mem_cases : (Σ a, z = inl a) + (Σ b, z = inr b) :=
by cases z with a b; exact inl ⟨a, idp⟩; exact inr ⟨b, idp⟩
protected definition eqrec {A B : Type} {C : A + B Type}
(x : A + B) (cl : Π a, x = inl a C (inl a)) (cr : Π b, x = inr b C (inr b)) : C x :=
by cases x with a b; exact cl a idp; exact cr b idp
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 [constructor] : (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)
/- Transport -/
definition sum_transport (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
/- Pathovers -/
definition etao (p : a = a') (z : P a + Q a)
: z =[p] sum.rec (λa, inl (p a)) (λb, inr (p b)) z :=
by induction p; induction z; all_goals constructor
protected definition codeo (p : a = a') : P a + Q a P a' + Q a' Type.{max u' v'}
| codeo (inl x) (inl x') := lift.{u' v'} (x =[p] x')
| codeo (inr y) (inr y') := lift.{v' u'} (y =[p] y')
| codeo _ _ := lift empty
protected definition decodeo (p : a = a') : Π(z : P a + Q a) (z' : P a' + Q a'),
sum.codeo p z z' z =[p] z'
| decodeo (inl x) (inl x') := λc, apo (λa, inl) (down c)
| decodeo (inl x) (inr y') := λc, empty.elim (down c) _
| decodeo (inr y) (inl x') := λc, empty.elim (down c) _
| decodeo (inr y) (inr y') := λc, apo (λa, inr) (down c)
variables {z z'}
protected definition encodeo {p : a = a'} {z : P a + Q a} {z' : P a' + Q a'} (q : z =[p] z')
: sum.codeo p z z' :=
by induction q; induction z; all_goals exact up idpo
variables (z z')
definition sum_pathover_equiv [constructor] (p : a = a') (z : P a + Q a) (z' : P a' + Q a')
: (z =[p] z') ≃ sum.codeo p z z' :=
equiv.MK sum.encodeo
!sum.decodeo
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 pathover
all_goals reflexivity
end end
abstract begin
intro q, induction q, induction z, all_goals reflexivity
end end
end
/- Functorial action -/
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)
infix ` +→ `:62 := sum_functor
/- Equivalences -/
definition is_equiv_sum_functor [constructor] [instance] [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 [constructor] [Hf : is_equiv f] [Hg : is_equiv g]
: A + B ≃ A' + B' :=
equiv.mk _ (is_equiv_sum_functor f g)
definition sum_equiv_sum [constructor] (f : A ≃ A') (g : B ≃ B') : A + B ≃ A' + B' :=
equiv.mk _ (is_equiv_sum_functor f g)
infix ` +≃ `:62 := sum_equiv_sum
definition sum_equiv_sum_left [constructor] (g : B ≃ B') : A + B ≃ A + B' :=
sum_equiv_sum equiv.rfl g
definition sum_equiv_sum_right [constructor] (f : A ≃ A') : A + B ≃ A' + B :=
sum_equiv_sum f equiv.rfl
definition flip [unfold 3] : A + B B + A
| flip (inl a) := inr a
| flip (inr b) := inl b
definition flip_flip (x : A ⊎ B) : flip (flip x) = x :=
begin induction x: reflexivity end
definition sum_comm_equiv [constructor] (A B : Type) : A + B ≃ B + A :=
equiv.MK flip flip flip_flip flip_flip
definition sum_assoc_equiv [constructor] (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),
exact inl (inl u),
exact inl (inr a),
exact inr a,
exact inl a,
exact inr (inl a),
exact inr (inr v),
all_goals reflexivity
end
definition sum_empty_equiv [constructor] (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 empty_sum_equiv [constructor] (A : Type) : empty + A ≃ A :=
!sum_comm_equiv e !sum_empty_equiv
definition bool_equiv_unit_sum_unit [constructor] : bool ≃ unit + unit :=
begin
fapply equiv.MK,
{ intro b, cases b, exact inl unit.star, exact inr unit.star },
{ intro s, cases s, exact bool.ff, exact bool.tt },
{ intro s, cases s, do 2 (cases a; reflexivity) },
{ intro b, cases b, do 2 reflexivity },
end
definition sum_prod_right_distrib [constructor] (A B C : Type) :
(A + B) × C ≃ (A × C) + (B × C) :=
begin
fapply equiv.MK,
{ intro x, cases x with ab c, cases ab with a b, exact inl (a, c), exact inr (b, c) },
{ intro x, cases x with ac bc, cases ac with a c, exact (inl a, c),
cases bc with b c, exact (inr b, c) },
{ intro x, cases x with ac bc, cases ac with a c, reflexivity, cases bc, reflexivity },
{ intro x, cases x with ab c, cases ab with a b, do 2 reflexivity }
end
definition sum_prod_left_distrib [constructor] (A B C : Type) :
A × (B + C) ≃ (A × B) + (A × C) :=
calc A × (B + C) ≃ (B + C) × A : prod_comm_equiv
... ≃ (B × A) + (C × A) : sum_prod_right_distrib
... ≃ (A × B) + (C × A) : sum_equiv_sum_right !prod_comm_equiv
... ≃ (A × B) + (A × C) : sum_equiv_sum_left !prod_comm_equiv
section
variables (H : unit + A ≃ unit + B)
include H
open unit sigma.ops
definition unit_sum_equiv_cancel_map : A B :=
begin
intro a, cases sum.mem_cases (H (inr a)) with u b, rotate 1, exact b.1,
cases u with u Hu, cases sum.mem_cases (H (inl ⋆)) with u' b, rotate 1, exact b.1,
cases u' with u' Hu', exfalso, apply empty_of_inl_eq_inr,
calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
... = H⁻¹ (inl u') : {Hu'}
... = H⁻¹ (inl u) : is_prop.elim
... = H⁻¹ (H (inr a)) : {Hu⁻¹}
... = inr a : to_left_inv H (inr a)
end
definition unit_sum_equiv_cancel_inv (b : B) :
unit_sum_equiv_cancel_map H (unit_sum_equiv_cancel_map H⁻¹ᵉ b) = b :=
begin
esimp[unit_sum_equiv_cancel_map], apply sum.rec,
{ intro x, cases x with u Hu, esimp, apply sum.rec,
{ intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr,
calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
... = H⁻¹ (inl u') : ap H⁻¹ Hu'
... = H⁻¹ (inl u) : {!is_prop.elim}
... = H⁻¹ (H (inr _)) : {Hu⁻¹}
... = inr _ : to_left_inv H },
{ intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x,
{ cases x with u' Hu', cases u', apply eq_of_inr_eq_inr,
calc inr b' = H (inl ⋆) : Hb'⁻¹
... = H (H⁻¹ (inr b)) : (ap H Hu')⁻¹
... = inr b : to_right_inv H (inr b)},
{ exfalso, cases x with a Ha, apply empty_of_inl_eq_inr,
cases u, apply concat, apply Hu⁻¹, apply concat, rotate 1, apply !(to_right_inv H),
apply ap H,
apply concat, rotate 1, apply Ha⁻¹, apply ap inr, esimp,
apply sum.rec, intro x, exfalso, apply empty_of_inl_eq_inr,
apply concat, exact x.2⁻¹, apply Ha,
intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ Ha } } },
{ intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ _,
cases sum.mem_cases (H⁻¹ (inr b)) with x x,
{ cases x with u Hu, esimp, cases sum.mem_cases (H⁻¹ (inl ⋆)) with x x,
{ cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr,
calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹
... = H (inl u') : ap H Hu'
... = H (inl u) : by rewrite [is_prop.elim u' u]
... = H (H⁻¹ (inr b)) : ap H Hu⁻¹
... = inr b : to_right_inv H (inr b) },
{ cases x with a Ha, exfalso, apply empty_of_inl_eq_inr,
apply concat, rotate 1, exact Hb',
have Ha' : inl ⋆ = H (inr a), by apply !(to_right_inv H)⁻¹ ap H Ha,
apply concat Ha', apply ap H, apply ap inr, apply sum.rec,
intro x, cases x with u' Hu', esimp, apply sum.rec,
intro x, cases x with u'' Hu'', esimp, apply empty.rec,
intro x, cases x with a'' Ha'', esimp, krewrite Ha' at Ha'', apply eq_of_inr_eq_inr,
apply !(to_left_inv H)⁻¹ Ha'',
intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr,
apply Hu⁻¹ Ha'', } },
{ cases x with a' Ha', esimp, refine _ !(to_right_inv H), apply ap H,
apply Ha'⁻¹ } }
end
definition unit_sum_equiv_cancel : A ≃ B :=
begin
fapply equiv.MK, apply unit_sum_equiv_cancel_map H,
apply unit_sum_equiv_cancel_map H⁻¹ᵉ,
intro b, apply unit_sum_equiv_cancel_inv,
{ intro a, have H = (H⁻¹ᵉ)⁻¹ᵉ, from !equiv.symm_symm⁻¹, rewrite this at {2},
apply unit_sum_equiv_cancel_inv }
end
end
/- universal property -/
definition sum_rec_unc [unfold 5] {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 [constructor] (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 [constructor] (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 [constructor] (A B C : Type)
: (A C) × (B C) ≃ (A + B C) :=
!equiv_sum_rec
/- truncatedness -/
theorem is_trunc_sum (n : ℕ₋₂) (A B : Type) [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
theorem is_trunc_sum_excluded (n : ℕ₋₂) (A B : Type) [HA : is_trunc n A] [HB : is_trunc n B]
(H : A B empty) : is_trunc n (A + B) :=
begin
induction n with n IH,
{ exfalso, exact H !center !center},
{ clear IH, induction n with n IH,
{ apply is_prop.mk, intros x y,
induction x, all_goals induction y, all_goals esimp,
all_goals try (exfalso;apply H;assumption;assumption), all_goals apply ap _ !is_prop.elim},
{ apply is_trunc_sum}}
end
definition is_contr_sum_left (A : Type) {B : Type} [HA : is_contr A] (H : ¬B) :
is_contr (A + B) :=
is_contr.mk (inl !center)
(λx, sum.rec_on x (λa, ap inl !center_eq) (λb, empty.elim (H b)))
/-
Sums are equivalent to dependent sigmas where the first component is a bool.
The current construction only works for A and B in the same universe.
If we need it for A and B in different universes, we need to insert some lifts.
-/
definition sum_of_sigma_bool {A B : Type.{u}} (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.{u}} (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 [constructor] (A B : Type.{u})
: 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
variables {A₀₀ A₂₀ A₀₂ A₂₂ B₀₀ B₂₀ B₀₂ B₂₂ C C' : Type}
{f₁₀ : A₀₀ A₂₀} {f₁₂ : A₀₂ A₂₂} {f₀₁ : A₀₀ A₀₂} {f₂₁ : A₂₀ A₂₂}
{g₁₀ : B₀₀ B₂₀} {g₁₂ : B₀₂ B₂₂} {g₀₁ : B₀₀ B₀₂} {g₂₁ : B₂₀ B₂₂}
{h₀₁ : B₀₀ A₀₂} {h₂₁ : B₂₀ A₂₂}
open function
definition sum_rec_hsquare [unfold 16] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁)
(k : hsquare g₁₀ f₁₂ h₀₁ h₂₁) : hsquare (f₁₀ +→ g₁₀) f₁₂ (sum.rec f₀₁ h₀₁) (sum.rec f₂₁ h₂₁) :=
begin intro x, induction x with a b, exact h a, exact k b end
definition sum_functor_hsquare [unfold 19] (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁)
(k : hsquare g₁₀ g₁₂ g₀₁ g₂₁) : hsquare (f₁₀ +→ g₁₀) (f₁₂ +→ g₁₂) (f₀₁ +→ g₀₁) (f₂₁ +→ g₂₁) :=
sum_rec_hsquare (λa, ap inl (h a)) (λb, ap inr (k b))
definition sum_functor_compose (g : B C) (f : A B) (g' : B' C') (f' : A' B') :
(g ∘ f) +→ (g' ∘ f') ~ g +→ g' ∘ f +→ f' :=
begin intro x, induction x with a a': reflexivity end
definition sum_rec_sum_functor (g : B C) (g' : B' C) (f : A B) (f' : A' B') :
sum.rec g g' ∘ sum_functor f f' ~ sum.rec (g ∘ f) (g' ∘ f') :=
begin intro x, induction x with a a': reflexivity end
definition sum_rec_same_compose (g : B C) (f : A B) :
sum.rec (g ∘ f) (g ∘ f) ~ g ∘ sum.rec f f :=
begin intro x, induction x with a a': reflexivity end
definition sum_rec_same (f : A B) : sum.rec f f ~ f ∘ sum.rec id id :=
by exact sum_rec_same_compose f id
/- pointed sums. We arbitrarily choose (inl pt) as basepoint for the sum -/
open pointed
definition psum [constructor] (A B : Type*) : Type* :=
pointed.MK (A ⊎ B) (inl pt)
infixr ` +* `:30 := psum
end sum
open sum pi
namespace decidable
/- some properties about the inductive type `decidable`
decidable A is equivalent to A + ¬A -/
definition decidable_equiv [constructor] (A : Type) : decidable A ≃ A + ¬A :=
begin
fapply equiv.MK:intro a;induction a:try (constructor;assumption;now),
all_goals reflexivity
end
definition is_trunc_decidable [constructor] (A : Type) (n : ℕ₋₂) [H : is_trunc n A] :
is_trunc n (decidable A) :=
begin
apply is_trunc_equiv_closed_rev,
apply decidable_equiv,
induction n with n IH,
{ apply is_contr_sum_left, exact λna, na !center},
{ apply is_trunc_sum_excluded, exact λa na, na a}
end
definition double_neg_elim {A : Type} (H : decidable A) (p : ¬ ¬ A) : A :=
begin induction H, assumption, contradiction end
definition dite_true {C : Type} [H : decidable C] {A : Type}
{t : C A} {e : ¬ C A} (c : C) (H' : is_prop C) : dite C t e = t c :=
begin
induction H with H H,
exact ap t !is_prop.elim,
contradiction
end
definition dite_false {C : Type} [H : decidable C] {A : Type}
{t : C A} {e : ¬ C A} (c : ¬ C) : dite C t e = e c :=
begin
induction H with H H,
contradiction,
exact ap e !is_prop.elim,
end
definition decidable_eq_of_is_prop (A : Type) [is_prop A] : decidable_eq A :=
λa a', decidable.inl !is_prop.elim
definition decidable_eq_sigma [instance] {A : Type} (B : A Type) [HA : decidable_eq A]
[HB : Πa, decidable_eq (B a)] : decidable_eq (Σa, B a) :=
begin
intro v v', induction v with a b, induction v' with a' b',
cases HA a a' with p np,
{ induction p, cases HB a b b' with q nq,
induction q, exact decidable.inl idp,
apply decidable.inr, intro p, apply nq, apply @eq_of_pathover_idp A B,
exact change_path !is_prop.elim p..2 },
{ apply decidable.inr, intro p, apply np, exact p..1 }
end
open sum
definition decidable_eq_sum [instance] (A B : Type) [HA : decidable_eq A] [HB : decidable_eq B] :
decidable_eq (A ⊎ B) :=
begin
intro v v', induction v with a b: induction v' with a' b',
{ cases HA a a' with p np,
{ exact decidable.inl (ap sum.inl p) },
{ apply decidable.inr, intro p, apply np, exact down (sum.encode p) }},
{ apply decidable.inr, intro p, cases p },
{ apply decidable.inr, intro p, cases p },
{ cases HB b b' with p np,
{ exact decidable.inl (ap sum.inr p) },
{ apply decidable.inr, intro p, apply np, exact down (sum.encode p) }},
end
end decidable
attribute sum.is_trunc_sum [instance] [priority 1480]
definition tsum [constructor] {n : ℕ₋₂} (A B : (n.+2)-Type) : (n.+2)-Type :=
trunctype.mk (A + B) _
infixr `+t`:25 := tsum