From 7c81044a9977a2063551bf5b211b911741ee6d7f Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Wed, 26 Nov 2014 16:53:41 -0500 Subject: [PATCH] chore(library/hott) change is_pointed to structure --- library/hott/pointed.lean | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/library/hott/pointed.lean b/library/hott/pointed.lean index d151c5f08..e5d633286 100644 --- a/library/hott/pointed.lean +++ b/library/hott/pointed.lean @@ -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