blob: 4e0e9c99881268b907dda80eeeecfd03023d5f59 (
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
|
module Obs.Sort
import Data.Bool
import Data.Nat
import Data.So
import Decidable.Equality
import Text.PrettyPrint.Prettyprinter
%default total
-- Definition ------------------------------------------------------------------
public export
data Sort : Type where
Prop : Sort
Set : Nat -> Sort
%name Sort s, s', s'', s'''
public export
toNat : Sort -> Nat
toNat Prop = 0
toNat (Set i) = S i
-- Interfaces ------------------------------------------------------------------
public export
Eq Sort where
Prop == Prop = True
(Set i) == (Set j) = i == j
_ == _ = False
public export
Ord Sort where
compare = compare `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 Sort 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 Sort where
show Prop = "Prop"
show (Set 0) = "Set"
show (Set (S i)) = "Set \{show (S i)}"
export
Pretty Sort 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 ~>
public export
isSet : Sort -> Bool
isSet = (> 0) . toNat
public export
suc : Sort -> Sort
suc = Set . toNat
public export
ensureSet : Sort -> Sort
ensureSet = max (Set 0)
public export
(~>) : Sort -> Sort -> Sort
s ~> Prop = Prop
s ~> (Set k) = max (Set k) s
-- Properties ------------------------------------------------------------------
export
maxIsSet : (s, s' : Sort) -> isSet (max s s') = isSet s || isSet s'
maxIsSet Prop s = Refl
maxIsSet (Set _) s = Refl
export
impredicative : (s, s' : Sort) -> isSet (s ~> s') = isSet s'
impredicative s Prop = Refl
impredicative s (Set i) = Refl
export
ensureSetIsSet : (s : Sort) -> So (isSet (ensureSet s))
ensureSetIsSet s = Oh
|
