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

fix(library/hott) changed pointed.lean to use trunc.lean correctly

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-12 18:01:01 -05:00 committed by Leonardo de Moura
parent 8dfa78e070
commit b514a978b2
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/hott/pointed.lean
View file

@ -4,20 +4,20 @@
-- Ported from Coq HoTT -- Ported from Coq HoTT
import hott.path hott.trunc data.sigma data.prod import hott.path hott.trunc data.sigma data.prod
open path prod open path prod truncation
inductive is_pointed [class] (A : Type) := inductive is_pointed [class] (A : Type) :=
pointed_mk : Π(a : A), is_pointed A pointed_mk : Π(a : A), is_pointed A
namespace is_pointed namespace is_pointed
variables {A B : Type} (f : A → B) variables {A B : Type.{1}} (f : A → B)
definition point (A : Type) [H : is_pointed A] : A := definition point (A : Type) [H : is_pointed A] : A :=
is_pointed.rec (λinv, inv) H is_pointed.rec (λinv, inv) H
-- Any contractible type is pointed -- Any contractible type is pointed
protected definition contr [instance] (H : Contr A) : is_pointed A := protected definition contr [instance] [H : is_contr A] : is_pointed A :=
pointed_mk (center H) pointed_mk (center A)
-- A pi type with a pointed target is pointed -- A pi type with a pointed target is pointed
protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)] protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]