blob: 14cde145ca7fdb3cfd8b9049172935c48fb2717d (
plain)
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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
||| Provides definitions of proof-relevance and type universes.
module Obs.Universe
import Data.Bool
import Data.Bool.Decidable
import Data.Nat
import Data.Nat.Order.Properties
import Data.So
import Decidable.Equality
import Text.PrettyPrint.Prettyprinter
%default total
-- Definition ------------------------------------------------------------------
||| Proof relevance of terms
public export
data Relevance = Irrelevant | Relevant
%name Relevance r, r'
||| Type universes.
public export
data Universe : Type where
||| Impredicative universe of strict propositions.
Prop : Universe
||| Predicative hierarchy of universes.
Set : Nat -> Universe
%name Universe s, s', s'', s'''
||| Converts universes to naturals as a helper for writing implementations.
public export
toNat : Universe -> Nat
toNat Prop = 0
toNat (Set i) = S i
-- Interfaces ------------------------------------------------------------------
public export
Eq Relevance where
Irrelevant == Irrelevant = True
Relevant == Relevant = True
_ == _ = False
export
Uninhabited (Irrelevant = Relevant) where uninhabited Refl impossible
export
Uninhabited (Relevant = Irrelevant) where uninhabited Refl impossible
export
DecEq Relevance where
decEq Irrelevant Irrelevant = Yes Refl
decEq Irrelevant Relevant = No absurd
decEq Relevant Irrelevant = No absurd
decEq Relevant Relevant = Yes Refl
public export
Eq Universe where
(==) = (==) `on` toNat
public export
Ord Universe where
compare = compare `on` toNat
(<) = lt `on` toNat
(>) = gt `on` toNat
(<=) = lte `on` toNat
(>=) = gte `on` toNat
min Prop s' = Prop
min (Set _) Prop = Prop
min (Set i) (Set j) = Set (minimum i j)
max Prop s' = s'
max (Set i) s' = Set (maximum i (pred $ toNat s'))
export
Uninhabited (Prop = Set i) where uninhabited Refl impossible
export
Uninhabited (Set i = Prop) where uninhabited Refl impossible
export
Injective Set where
injective Refl = Refl
public export
DecEq Universe where
decEq Prop Prop = Yes Refl
decEq Prop (Set _) = No absurd
decEq (Set _) Prop = No absurd
decEq (Set i) (Set j) = decEqCong $ decEq i j
export
Show Universe where
showPrec d Prop = "Prop"
showPrec d (Set 0) = "Set"
showPrec d (Set (S i)) = showParens (d >= App) $ "Set \{show (S i)}"
export
Pretty Universe where
prettyPrec d Prop = pretty "Prop"
prettyPrec d (Set 0) = pretty "Set"
prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"
-- Operations ------------------------------------------------------------------
infixr 5 ~>
||| Computes the proof-relevance of a pair.
public export
pair : (fst, snd : Relevance) -> Relevance
pair Irrelevant = id
pair Relevant = const Relevant
||| Computes the proof-relevance of a function.
public export
function : (dom, cod : Relevance) -> Relevance
function = const id
||| Gets the proof-relevance of values in a universe.
public export
relevance : Universe -> Relevance
relevance Prop = Irrelevant
relevance (Set k) = Relevant
||| Returns the smallest universe containing `s`
||| @ s the universe to contain
public export
succ : (s : Universe) -> Universe
succ = Set . toNat
||| The universe of a dependent product.
||| @ dom the domain universe
||| @ cod the codomain universe
public export
(~>) : (dom, cod : Universe) -> Universe
dom ~> Prop = Prop
dom ~> (Set k) = max (Set k) dom
-- Views -----------------------------------------------------------------------
namespace Predicates
public export
data IsIrrelevant : Relevance -> Type where
Irrelevant : IsIrrelevant Irrelevant
public export
data IsRelevant : Relevance -> Type where
Relevant : IsRelevant Relevant
export
Uninhabited (IsIrrelevant Relevant) where
uninhabited _ impossible
export
Uninhabited (IsRelevant Irrelevant) where
uninhabited _ impossible
export
isIrrelevant : (r : Relevance) -> Dec (IsIrrelevant r)
isIrrelevant Irrelevant = Yes Irrelevant
isIrrelevant Relevant = No absurd
export
isRelevant : (r : Relevance) -> Dec (IsRelevant r)
isRelevant Irrelevant = No absurd
isRelevant Relevant = Yes Relevant
-- Properties ------------------------------------------------------------------
export
pairRelevantRight : (fst : Relevance) -> pair fst Relevant = Relevant
pairRelevantRight Irrelevant = Refl
pairRelevantRight Relevant = Refl
succContains : (s : Universe) -> So (s < succ s)
succContains Prop = Oh
succContains (Set k) = eqToSo $ LteIslte k k reflexive
succLeast : (s, s' : Universe) -> So (s < s') -> So (succ s <= s')
succLeast s s' prf = prf
export
pairRelevance : (s, s' : Universe) -> relevance (max s s') = pair (relevance s) (relevance s')
pairRelevance Prop s' = Refl
pairRelevance (Set k) s' = Refl
export
functionRelevance : (s, s' : Universe) ->
relevance (s ~> s') = function (relevance s) (relevance s')
functionRelevance s Prop = Refl
functionRelevance s (Set k) = Refl
|
