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

chore(library/hott) change is_pointed to structure

Browse source
This commit is contained in:
Jakob von Raumer 2014-11-26 16:53:41 -05:00 committed by Leonardo de Moura
parent 0417c21bbb
commit 7c81044a99
1 changed files with 8 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
library/hott/pointed.lean
View file

@ -6,34 +6,31 @@ import hott.path hott.trunc data.sigma data.prod
open path prod truncation
inductive is_pointed [class] (A : Type) :=
pointed_mk : Π(a : A), is_pointed A
structure is_pointed [class] (A : Type) :=
(point : A)
namespace is_pointed
variables {A B : Type.{1}} (f : A → B)
definition point (A : Type) [H : is_pointed A] : A :=
is_pointed.rec (λinv, inv) H
variables {A B : Type} (f : A → B)
-- Any contractible type is pointed
protected definition contr [instance] [H : is_contr A] : is_pointed A :=
pointed_mk (center A)
is_pointed.mk (center A)
-- A pi type with a pointed target is pointed
protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]
: is_pointed (Πx, P x) :=
pointed_mk (λx, point (P x))
is_pointed.mk (λx, point (P x))
-- 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) :=
pointed_mk (sigma.dpair (point A) (point (P (point A))))
is_pointed.mk (sigma.dpair (point A) (point (P (point A))))
protected definition prod [H1 : is_pointed A] [H2 : is_pointed B]
: is_pointed (A × B) :=
pointed_mk (prod.mk (point A) (point B))
is_pointed.mk (prod.mk (point A) (point B))
protected definition loop_space (a : A) : is_pointed (a ≈ a) :=
pointed_mk idp
is_pointed.mk idp
end is_pointed