lean2/hott/hit/trunc.hlean

140 lines
5 KiB
Text
Raw Normal View History

/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: hit.trunc
Authors: Floris van Doorn
n-truncation of types.
Ported from Coq HoTT
-/
/- The hit n-truncation is primitive, declared in init.hit. -/
import types.sigma
open is_trunc eq equiv is_equiv function prod sum sigma
namespace trunc
protected definition elim {n : trunc_index} {A : Type} {P : Type}
[Pt : is_trunc n P] (H : A → P) : trunc n A → P :=
trunc.rec H
protected definition elim_on {n : trunc_index} {A : Type} {P : Type} (aa : trunc n A)
[Pt : is_trunc n P] (H : A → P) : P :=
elim H aa
/-
there are no theorems to eliminate to the universe here,
because the universe is generally not a set
-/
--export is_trunc
variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index)
local attribute is_trunc_eq [instance]
definition is_equiv_tr [instance] [H : is_trunc n A] : is_equiv (@tr n A) :=
adjointify _
(trunc.rec id)
(λaa, trunc.rec_on aa (λa, idp))
(λa, idp)
definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A :=
equiv.mk tr _
definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A :=
is_trunc_is_equiv_closed n tr⁻¹
definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A :=
tr⁻¹
/- Functoriality -/
definition trunc_functor (f : X → Y) : trunc n X → trunc n Y :=
λxx, trunc.rec_on xx (λx, tr (f x))
-- by intro xx; apply (trunc.rec_on xx); intro x; exact (tr (f x))
-- by intro xx; fapply (trunc.rec_on xx); intro x; exact (tr (f x))
-- by intro xx; exact (trunc.rec_on xx (λx, (tr (f x))))
definition trunc_functor_compose (f : X → Y) (g : Y → Z)
: trunc_functor n (g ∘ f) trunc_functor n g ∘ trunc_functor n f :=
λxx, trunc.rec_on xx (λx, idp)
definition trunc_functor_id : trunc_functor n (@id A) id :=
λxx, trunc.rec_on xx (λx, idp)
definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) :=
adjointify _
(trunc_functor n f⁻¹)
(λyy, trunc.rec_on yy (λy, ap tr !right_inv))
(λxx, trunc.rec_on xx (λx, ap tr !left_inv))
section
open prod.ops
definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
sorry
-- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))
-- (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y))))
-- sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp)))
-- (λpp, trunc.rec_on pp (λp, prod.rec_on p (λx y, idp)))
-- begin
-- fapply equiv.MK,
-- apply sorry, --{exact (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))},
-- apply sorry, /-{intro p, cases p with xx yy,
-- apply (trunc.rec_on xx), intro x,
-- apply (trunc.rec_on yy), intro y, exact (tr (x,y))},-/
-- apply sorry, /-{intro p, cases p with xx yy,
-- apply (trunc.rec_on xx), intro x,
-- apply (trunc.rec_on yy), intro y, apply idp},-/
-- apply sorry --{intro pp, apply (trunc.rec_on pp), intro p, cases p, apply idp},
-- end
end
/- Propositional truncation -/
-- should this live in hprop?
definition merely [reducible] (A : Type) : Type := trunc -1 A
notation `||`:max A `||`:0 := merely A
notation `∥`:max A `∥`:0 := merely A
definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥
definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
notation A `\/` B := or A B
notation A B := or A B
definition merely.intro [reducible] (a : A) : ∥ A ∥ := tr a
definition exists.intro [reducible] (x : X) (p : P x) : ∃x, P x := tr ⟨x, p⟩
definition or.intro_left [reducible] (x : X) : X Y := tr (inl x)
definition or.intro_right [reducible] (y : Y) : X Y := tr (inr y)
definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A :=
is_contr_of_inhabited_hprop (trunc.rec_on aa id)
section
open sigma.ops
definition trunc_sigma_equiv : trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) :=
equiv.MK (λpp, trunc.rec_on pp (λp, tr ⟨p.1, tr p.2⟩))
(λpp, trunc.rec_on pp (λp, trunc.rec_on p.2 (λb, tr ⟨p.1, b⟩)))
(λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa bb, trunc.rec_on bb (λb, by esimp))))
(λpp, trunc.rec_on pp (λp, sigma.rec_on p (λa b, by esimp)))
definition trunc_sigma_equiv_of_is_trunc [H : is_trunc n X]
: trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) :=
calc
trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv
... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc
end
end trunc
attribute trunc.elim [unfold-c 6]
attribute trunc.elim_on [unfold-c 4]