forked from leanprover/lean2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpointed.hlean
160 lines (113 loc) · 4.97 KB
/
pointed.hlean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
/-
Copyright (c) 2016 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
The definition of pointed types. This file is here to avoid circularities in the import graph
-/
prelude
import init.trunc
open eq equiv is_equiv is_trunc
structure pointed [class] (A : Type) :=
(point : A)
structure pType :=
(carrier : Type)
(Point : carrier)
notation `Type*` := pType
namespace pointed
attribute pType.carrier [coercion]
variables {A : Type}
definition pt [reducible] [unfold 2] [H : pointed A] := point A
definition Point [reducible] [unfold 1] (A : Type*) := pType.Point A
definition carrier [reducible] [unfold 1] (A : Type*) := pType.carrier A
protected definition Mk [constructor] {A : Type} (a : A) := pType.mk A a
protected definition MK [constructor] (A : Type) (a : A) := pType.mk A a
protected definition mk' [constructor] (A : Type) [H : pointed A] : Type* :=
pType.mk A (point A)
definition pointed_carrier [instance] [constructor] (A : Type*) : pointed A :=
pointed.mk (Point A)
end pointed
open pointed
section
universe variable u
structure ptrunctype (n : ℕ₋₂) extends trunctype.{u} n, pType.{u}
definition is_trunc_ptrunctype [instance] {n : ℕ₋₂} (X : ptrunctype n)
: is_trunc n (ptrunctype.to_pType X) :=
trunctype.struct X
end
notation n `-Type*` := ptrunctype n
abbreviation pSet [parsing_only] := 0-Type*
notation `Set*` := pSet
namespace pointed
protected definition ptrunctype.mk' [constructor] (n : ℕ₋₂)
(A : Type) [pointed A] [is_trunc n A] : n-Type* :=
ptrunctype.mk A _ pt
protected definition pSet.mk [constructor] := @ptrunctype.mk (-1.+1)
protected definition pSet.mk' [constructor] := ptrunctype.mk' (-1.+1)
definition ptrunctype_of_trunctype [constructor] {n : ℕ₋₂} (A : n-Type) (a : A)
: n-Type* :=
ptrunctype.mk A _ a
definition ptrunctype_of_pType [constructor] {n : ℕ₋₂} (A : Type*) (H : is_trunc n A)
: n-Type* :=
ptrunctype.mk A _ pt
definition pSet_of_Set [constructor] (A : Set) (a : A) : Set* :=
ptrunctype.mk A _ a
definition pSet_of_pType [constructor] (A : Type*) (H : is_set A) : Set* :=
ptrunctype.mk A _ pt
attribute ptrunctype._trans_of_to_pType ptrunctype.to_pType ptrunctype.to_trunctype [unfold 2]
-- Any contractible type is pointed
definition pointed_of_is_contr [instance] [priority 800] [constructor]
(A : Type) [H : is_contr A] : pointed A :=
pointed.mk !center
end pointed
/- pointed maps -/
structure ppi {A : Type*} (P : A → Type) (x₀ : P pt) :=
(to_fun : Π a : A, P a)
(resp_pt : to_fun (Point A) = x₀)
definition pppi' [reducible] {A : Type*} (P : A → Type*) : Type :=
ppi P pt
definition ppi_const [constructor] {A : Type*} (P : A → Type*) : pppi' P :=
ppi.mk (λa, pt) idp
definition pppi [constructor] [reducible] {A : Type*} (P : A → Type*) : Type* :=
pointed.MK (pppi' P) (ppi_const P)
-- do we want to make this already pointed?
definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B)
attribute ppi.to_fun [coercion]
infix ` →* `:28 := pmap
notation `Π*` binders `, ` r:(scoped P, pppi P) := r
namespace pointed
definition pppi.mk [constructor] [reducible] {A : Type*} {P : A → Type*} (f : Πa, P a)
(p : f pt = pt) : pppi P :=
ppi.mk f p
definition pppi.to_fun [unfold 3] [coercion] [reducible] {A : Type*} {P : A → Type*} (f : pppi' P)
(a : A) : P a :=
ppi.to_fun f a
definition pmap.mk [constructor] [reducible] {A B : Type*} (f : A → B)
(p : f (Point A) = Point B) : A →* B :=
pppi.mk f p
abbreviation pmap.to_fun [unfold 3] [reducible] [coercion] {A B : Type*} (f : A →* B) : A → B :=
pppi.to_fun f
definition respect_pt [unfold 4] [reducible] {A : Type*} {P : A → Type} {p₀ : P pt}
(f : ppi P p₀) : f pt = p₀ :=
ppi.resp_pt f
-- notation `Π*` binders `, ` r:(scoped P, ppi _ P) := r
-- definition pmxap.mk [constructor] {A B : Type*} (f : A → B) (p : f pt = pt) : A →* B :=
-- ppi.mk f p
-- definition pmap.to_fun [coercion] [unfold 3] {A B : Type*} (f : A →* B) : A → B := f
end pointed open pointed
/- pointed homotopies -/
definition phomotopy {A : Type*} {P : A → Type} {p₀ : P pt} (f g : ppi P p₀) : Type :=
ppi (λa, f a = g a) (respect_pt f ⬝ (respect_pt g)⁻¹)
-- structure phomotopy {A B : Type*} (f g : A →* B) : Type :=
-- (homotopy : f ~ g)
-- (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
namespace pointed
variables {A : Type*} {P : A → Type} {p₀ : P pt} {f g : ppi P p₀}
infix ` ~* `:50 := phomotopy
definition phomotopy.mk [reducible] [constructor] (h : f ~ g)
(p : h pt ⬝ respect_pt g = respect_pt f) : f ~* g :=
ppi.mk h (eq_con_inv_of_con_eq p)
definition to_homotopy [coercion] [unfold 5] [reducible] (p : f ~* g) : Πa, f a = g a := p
definition to_homotopy_pt [unfold 5] [reducible] (p : f ~* g) :
p pt ⬝ respect_pt g = respect_pt f :=
con_eq_of_eq_con_inv (respect_pt p)
end pointed