summaryrefslogtreecommitdiff
path: root/src/Obs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Obs')
-rw-r--r--src/Obs/Abstract.idr2
-rw-r--r--src/Obs/Main.idr1
-rw-r--r--src/Obs/NormalForm.idr107
-rw-r--r--src/Obs/NormalForm/Normalise.idr223
-rw-r--r--src/Obs/Parser.idr20
-rw-r--r--src/Obs/Sort.idr110
-rw-r--r--src/Obs/Syntax.idr8
-rw-r--r--src/Obs/Term.idr8
-rw-r--r--src/Obs/Typing.idr92
-rw-r--r--src/Obs/Typing/Context.idr40
-rw-r--r--src/Obs/Typing/Conversion.idr90
-rw-r--r--src/Obs/Universe.idr222
12 files changed, 521 insertions, 402 deletions
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index b32af2d..a9ef411 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -25,7 +25,7 @@ abstractSyntax ctx (Var var) = do
let Just i = lookup var ctx
| Nothing => inScope "unbound variable" $ fatal var
pure (Var var i)
-abstractSyntax ctx (Sort s) = pure (Sort s)
+abstractSyntax ctx (Universe s) = pure (Universe s)
abstractSyntax ctx (Pi var a b) = do
a <- abstractSyntaxBounds ctx a
b <- abstractSyntaxBounds (bind ctx var.val) b
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 4d7c856..7162a20 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -9,6 +9,7 @@ import Obs.Parser
import Obs.Syntax
import Obs.Term
import Obs.Typing
+import Obs.Universe
import System
import System.File
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index a756728..d660111 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -1,10 +1,9 @@
module Obs.NormalForm
import Data.List.Elem
-import Data.So
-import Obs.Sort
import Obs.Substitution
+import Obs.Universe
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
@@ -13,29 +12,33 @@ import Text.PrettyPrint.Prettyprinter
-- Definition ------------------------------------------------------------------
-data NormalForm : Sorted.Family Bool
+data NormalForm : Sorted.Family Relevance
public export
-data Constructor : Unsorted.Family Bool where
- Sort : (s : Sort) -> Constructor ctx
- Pi : (s, s' : Sort)
+TypeNormalForm : Unsorted.Family Relevance
+TypeNormalForm = NormalForm Relevant
+
+public export
+data Constructor : Unsorted.Family Relevance where
+ Universe : (s : Universe) -> Constructor ctx
+ Pi : (s, s' : Universe)
-> (var : String)
- -> (a : NormalForm True ctx)
- -> (b : NormalForm True (isSet s :: ctx))
+ -> (a : TypeNormalForm ctx)
+ -> (b : TypeNormalForm (relevance s :: ctx))
-> Constructor ctx
- Lambda : (s : Sort)
+ Lambda : (s : Universe)
-> (var : String)
- -> NormalForm True (isSet s :: ctx)
+ -> NormalForm Relevant (relevance s :: ctx)
-> Constructor ctx
- Sigma : (s, s' : Sort)
+ Sigma : (s, s' : Universe)
-> (var : String)
- -> (a : NormalForm True ctx)
- -> (b : NormalForm True (isSet s :: ctx))
+ -> (a : TypeNormalForm ctx)
+ -> (b : TypeNormalForm (relevance s :: ctx))
-> Constructor ctx
- Pair : (s, s' : Sort)
- -> (prf : So (isSet (max s s')))
- -> NormalForm (isSet s) ctx
- -> NormalForm (isSet s') ctx
+ Pair : (s, s' : Universe)
+ -> (prf : IsRelevant (max s s'))
+ -> NormalForm (relevance s) ctx
+ -> NormalForm (relevance s') ctx
-> Constructor ctx
Bool : Constructor ctx
True : Constructor ctx
@@ -44,61 +47,61 @@ data Constructor : Unsorted.Family Bool where
Bottom : Constructor ctx
public export
-data Neutral : Unsorted.Family Bool where
+data Neutral : Unsorted.Family Relevance where
Var : (var : String)
- -> (sort : Sort)
- -> (prf : So (isSet sort))
- -> (i : Elem True ctx)
+ -> (sort : Universe)
+ -> (prf : IsRelevant sort)
+ -> (i : Elem Relevant ctx)
-> Neutral ctx
- App : (b : Bool) -> Neutral ctx -> NormalForm b ctx -> Neutral ctx
- Fst : (b : Bool) -> Neutral ctx -> Neutral ctx
- Snd : (b : Bool) -> Neutral ctx -> Neutral ctx
- If : Neutral ctx -> (f, g : NormalForm True ctx) -> Neutral ctx
+ App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx
+ Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx
+ Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx
+ If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx
Absurd : Neutral ctx
- Equal : Neutral ctx -> NormalForm True ctx -> NormalForm True ctx -> Neutral ctx
- EqualL : (a : Neutral ctx) -> (b : NormalForm True ctx) -> Neutral ctx
+ Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx
+ EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx
EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
CastL : (a : Neutral ctx) ->
- (b : NormalForm True ctx) ->
- NormalForm True ctx ->
+ (b : TypeNormalForm ctx) ->
+ NormalForm Relevant ctx ->
Neutral ctx
- CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm True ctx -> Neutral ctx
- CastStuck : (a, b : Constructor ctx) -> NormalForm True ctx -> Neutral ctx
+ CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx
+ CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx
public export
-data NormalForm : Sorted.Family Bool where
- Ntrl : Neutral ~|> NormalForm True
- Cnstr : Constructor ~|> NormalForm True
- Irrel : NormalForm False ctx
+data NormalForm : Sorted.Family Relevance where
+ Ntrl : Neutral ~|> NormalForm Relevant
+ Cnstr : Constructor ~|> NormalForm Relevant
+ Irrel : NormalForm Irrelevant ctx
%name Constructor t, u, v
%name Neutral t, u, v
%name NormalForm t, u, v
public export
-record Definition (ctx : List Bool) where
+record Definition (ctx : List Relevance) where
constructor MkDefinition
name : WithBounds String
- sort : Sort
- ty : NormalForm True ctx
- tm : NormalForm (isSet sort) ctx
+ sort : Universe
+ ty : TypeNormalForm ctx
+ tm : NormalForm (relevance sort) ctx
public export
-data Context : List Bool -> Type where
+data Context : List Relevance -> Type where
Nil : Context []
- (:<) : Context ctx -> (def : Definition ctx) -> Context (isSet def.sort :: ctx)
+ (:<) : Context ctx -> (def : Definition ctx) -> Context (relevance def.sort :: ctx)
%name Context ctx, ctx', ctx''
-- Convenience Casts -----------------------------------------------------------
public export
-Cast Sort (Constructor ctx) where
- cast s = Sort s
+Cast Universe (Constructor ctx) where
+ cast s = Universe s
public export
-Cast Sort (NormalForm True ctx) where
+Cast Universe (NormalForm Relevant ctx) where
cast s = Cnstr $ cast s
-- Pretty Print ----------------------------------------------------------------
@@ -106,7 +109,7 @@ Cast Sort (NormalForm True ctx) where
prettyPrec : Prec -> NormalForm b ctx -> Doc ann
prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
-prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d (Universe s) = prettyPrec d s
prettyPrecCnstr d (Pi s s' var a b) =
let lhs = case var of
"" => align (prettyPrec App a)
@@ -208,7 +211,7 @@ Pretty (NormalForm b ctx) where
rename : NormalForm ~|> Hom Elem NormalForm
renameCnstr : Constructor ~|> Hom Elem Constructor
-renameCnstr (Sort s) f = Sort s
+renameCnstr (Universe s) f = Universe s
renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
renameCnstr (Sigma s s' var a b) f =
@@ -240,18 +243,18 @@ rename (Cnstr t) f = Cnstr $ renameCnstr t f
rename Irrel f = Irrel
export
-Unsorted.Rename Bool Constructor where
+Unsorted.Rename Relevance Constructor where
rename = renameCnstr
export
-Unsorted.Rename Bool Neutral where
+Unsorted.Rename Relevance Neutral where
rename = renameNtrl
export
-Sorted.Rename Bool NormalForm where
+Sorted.Rename Relevance NormalForm where
rename = NormalForm.rename
export
-PointedRename Bool (\b => (String, (s : Sort ** isSet s = b))) NormalForm where
- point {s = False} _ _ = Irrel
- point {s = True} (var, (s ** prf)) i = Ntrl (Var var s (eqToSo prf) i)
+PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where
+ point {s = Irrelevant} _ _ = Irrel
+ point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i)
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 82e84b9..ed06fa2 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -1,14 +1,14 @@
module Obs.NormalForm.Normalise
import Data.Bool
-import Data.So
+import Data.Nat
import Decidable.Equality
import Obs.Logging
import Obs.NormalForm
-import Obs.Sort
import Obs.Substitution
+import Obs.Universe
import Text.PrettyPrint.Prettyprinter
@@ -17,19 +17,19 @@ import Text.PrettyPrint.Prettyprinter
-- Aliases ---------------------------------------------------------------------
public export 0
-LogConstructor : Type -> Unsorted.Family Bool
+LogConstructor : Type -> Unsorted.Family Relevance
LogConstructor ann ctx = Logging ann (Constructor ctx)
public export 0
-LogNormalForm : Type -> Sorted.Family Bool
+LogNormalForm : Type -> Sorted.Family Relevance
LogNormalForm ann b ctx = Logging ann (NormalForm b ctx)
0
-LogNormalForm' : Type -> Sorted.Family Bool
+LogNormalForm' : Type -> Sorted.Family Relevance
LogNormalForm' ann b ctx = Either (Logging ann (NormalForm b ctx)) (Elem b ctx)
-- Copied and specialised from Obs.Substitution
-lift : (ctx : List (b ** (String, (s ** isSet s = b))))
+lift : (ctx : List (r ** (String, (s ** relevance s = r))))
-> Map ctx' (LogNormalForm' ann) ctx''
-> Map (map DPair.fst ctx ++ ctx') (LogNormalForm' ann) (map DPair.fst ctx ++ ctx'')
lift [] f = f
@@ -42,184 +42,187 @@ lift ((s ** y) :: ctx) f = add (LogNormalForm' ann)
subst' : NormalForm ~|> Hom (LogNormalForm' ann) (LogNormalForm ann)
export
-doApp : {b' : _} -> NormalForm b ctx -> NormalForm b' ctx -> LogNormalForm ann b ctx
+doApp : {domain : _} ->
+ NormalForm (function domain codomain) ctx ->
+ NormalForm domain ctx ->
+ LogNormalForm ann codomain ctx
doApp (Ntrl t) u = pure (Ntrl $ App _ t u)
doApp (Cnstr (Lambda s var t)) u = inScope "doApp" $ do
trace $ pretty {ann} "substituting" <++> pretty u <+> softline <+> pretty "for \{var} in" <++> pretty t
- let Yes Refl = decEq b' (isSet s)
- | No _ => fatal "internal sort mismatch"
+ let Yes Refl = decEq domain (relevance s)
+ | No _ => fatal "internal relevance mismatch"
subst' t (add (LogNormalForm' ann) (Left $ pure u) Right)
doApp (Cnstr t) u = inScope "wrong constructor for apply" $ fatal t
doApp Irrel u = pure Irrel
export
-doFst : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b ctx
-doFst False b' t = pure Irrel
-doFst True b' (Ntrl t) = pure (Ntrl $ Fst b' t)
-doFst True b' (Cnstr (Pair (Set _) s' prf t u)) = pure t
-doFst True b' (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
+doFst : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann fst ctx
+doFst Irrelevant snd t = pure Irrel
+doFst Relevant snd (Ntrl t) = pure (Ntrl $ Fst snd t)
+doFst Relevant snd (Cnstr (Pair (Set _) s' prf t u)) = pure t
+doFst Relevant snd (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
export
-doSnd : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b' ctx
-doSnd b False t = pure Irrel
-doSnd b True t =
- let t' : NormalForm True ctx
- t' = rewrite sym $ orTrueTrue b in t
+doSnd : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann snd ctx
+doSnd fst Irrelevant t = pure Irrel
+doSnd fst Relevant t =
+ let t' : NormalForm Relevant ctx
+ t' = rewrite sym $ pairRelevantRight fst in t
in case t' of
- Ntrl t => pure (Ntrl $ Snd b t)
+ Ntrl t => pure (Ntrl $ Snd fst t)
Cnstr (Pair _ (Set _) prf t u) => pure u
Cnstr t => inScope "wrong constructor for snd" $ fatal t
export
-doIf : {b : _} ->
- NormalForm True ctx ->
- NormalForm b ctx ->
- NormalForm b ctx ->
- LogNormalForm ann b ctx
-doIf {b = False} t u v = pure Irrel
-doIf {b = True} (Ntrl t) u v = pure (Ntrl $ If t u v)
-doIf {b = True} (Cnstr True) u v = pure u
-doIf {b = True} (Cnstr False) u v = pure v
-doIf {b = True} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t
+doIf : {r : _} ->
+ NormalForm Relevant ctx ->
+ NormalForm r ctx ->
+ NormalForm r ctx ->
+ LogNormalForm ann r ctx
+doIf {r = Irrelevant} t u v = pure Irrel
+doIf {r = Relevant} (Ntrl t) u v = pure (Ntrl $ If t u v)
+doIf {r = Relevant} (Cnstr True) u v = pure u
+doIf {r = Relevant} (Cnstr False) u v = pure v
+doIf {r = Relevant} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t
export
-doAbsurd : (b : _) -> NormalForm b ctx
-doAbsurd False = Irrel
-doAbsurd True = Ntrl Absurd
+doAbsurd : (r : _) -> NormalForm r ctx
+doAbsurd Irrelevant = Irrel
+doAbsurd Relevant = Ntrl Absurd
export
-doCast : (b' : _) -> (a, b : NormalForm True ctx) -> NormalForm b' ctx -> LogNormalForm ann b' ctx
+doCast : (r : _) -> (a, b : TypeNormalForm ctx) -> NormalForm r ctx -> LogNormalForm ann r ctx
doCastR : (a : Constructor ctx) ->
- (b : NormalForm True ctx) ->
- NormalForm True ctx ->
- LogNormalForm ann True ctx
+ (b : TypeNormalForm ctx) ->
+ NormalForm Relevant ctx ->
+ LogNormalForm ann Relevant ctx
doCastR a (Ntrl b) t = pure (Ntrl $ CastR a b t)
-doCastR (Sort _) (Cnstr (Sort _)) t = pure t
+doCastR (Universe _) (Cnstr (Universe _)) t = pure t
doCastR ty@(Pi s s'@(Set _) var a b) (Cnstr ty'@(Pi l l' _ a' b')) t =
- let y : NormalForm (isSet s) (isSet s :: ctx)
+ let y : NormalForm (relevance s) (relevance s :: ctx)
y = point (var, (s ** Refl)) Here
in do
let Yes Refl = decEq (s, s') (l, l')
| No _ => pure (Ntrl $ CastStuck ty ty' t)
- x <- assert_total (doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) y)
+ x <- assert_total (doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) y)
b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure x) (Right . There)))
b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure y) (Right . There)))
- t <- assert_total (doApp (Sorted.weaken [isSet s] t) x)
- t <- assert_total (doCast True b b' t)
+ t <- assert_total (doApp (Sorted.weaken [relevance s] t) x)
+ t <- assert_total (doCast Relevant b b' t)
pure (Cnstr $ Lambda s var t)
doCastR ty@(Sigma s@(Set k) s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) t = do
let Yes Refl = decEq (s, s') (l, l')
| No _ => pure (Ntrl $ CastStuck ty ty' t)
- t1 <- doFst True (isSet s') t
- u1 <- assert_total (doCast True a a' t)
+ t1 <- doFst Relevant (relevance s') t
+ u1 <- assert_total (doCast Relevant a a' t)
b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u1) Right))
- t2 <- doSnd True (isSet s') t
- u2 <- assert_total (doCast (isSet s') b b' t2)
- pure (Cnstr $ Pair (Set k) s' Oh u1 u2)
+ t2 <- doSnd Relevant (relevance s') t
+ u2 <- assert_total (doCast (relevance s') b b' t2)
+ pure (Cnstr $ Pair (Set k) s' Set u1 u2)
doCastR ty@(Sigma Prop s'@(Set k) var a b) (Cnstr ty'@(Sigma Prop l' _ a' b')) t = do
let Yes Refl = decEq s' l'
| No _ => pure (Ntrl $ CastStuck ty ty' t)
b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
- t2 <- doSnd False True t
- u2 <- assert_total (doCast True b b' t2)
- pure (Cnstr $ Pair Prop (Set k) Oh Irrel u2)
+ t2 <- doSnd Irrelevant Relevant t
+ u2 <- assert_total (doCast Relevant b b' t2)
+ pure (Cnstr $ Pair Prop (Set k) Set Irrel u2)
doCastR Bool (Cnstr Bool) t = pure t
doCastR a (Cnstr b) t = pure (Ntrl $ CastStuck a b t)
-doCast False a b t = pure Irrel
-doCast True (Ntrl a) b t = pure (Ntrl $ CastL a b t)
-doCast True (Cnstr a) b t = doCastR a b t
+doCast Irrelevant a b t = pure Irrel
+doCast Relevant (Ntrl a) b t = pure (Ntrl $ CastL a b t)
+doCast Relevant (Cnstr a) b t = doCastR a b t
export
-doEqual : (b : _) ->
- (a : NormalForm True ctx) ->
- NormalForm b ctx ->
- NormalForm b ctx ->
- LogNormalForm ann True ctx
+doEqual : (r : _) ->
+ (a : TypeNormalForm ctx) ->
+ NormalForm r ctx ->
+ NormalForm r ctx ->
+ LogNormalForm ann Relevant ctx
-- Relies heavily on typing
-doEqualR : (a : Constructor ctx) -> (b : NormalForm True ctx) -> LogNormalForm ann True ctx
+doEqualR : (a : Constructor ctx) -> (b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
doEqualR a (Ntrl b) = pure (Ntrl $ EqualR a b)
-doEqualR (Sort _) (Cnstr (Sort s)) = pure (Cnstr Top)
+doEqualR (Universe _) (Cnstr (Universe s)) = pure (Cnstr Top)
doEqualR ty@(Pi s s' var a b) (Cnstr ty'@(Pi l l' _ a' b')) =
- let u : NormalForm (isSet s) (isSet s :: ctx)
+ let u : NormalForm (relevance s) (relevance s :: ctx)
u = point (var, (s ** Refl)) Here
in do
let Yes Refl = decEq (s, s') (l, l')
| No _ => pure (Ntrl $ EqualStuck ty ty')
- eq1 <- assert_total (doEqual True (cast s) a' a)
- t <- doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) u
+ eq1 <- assert_total (doEqual Relevant (cast s) a' a)
+ t <- doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) u
b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
- eq2 <- assert_total (doEqual True (cast s') b b')
- pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2))
+ eq2 <- assert_total (doEqual Relevant (cast s') b b')
+ pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
doEqualR ty@(Sigma s s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) =
- let t : NormalForm (isSet s) (isSet s :: ctx)
+ let t : NormalForm (relevance s) (relevance s :: ctx)
t = point (var, (s ** Refl)) Here
in do
let Yes Refl = decEq (s, s') (l, l')
| No _ => pure (Ntrl $ EqualStuck ty ty')
- eq1 <- assert_total (doEqual True (cast s) a a')
- u <- doCast (isSet s) (weaken [isSet s] a) (weaken [isSet s] a') t
+ eq1 <- assert_total (doEqual Relevant (cast s) a a')
+ u <- doCast (relevance s) (weaken [relevance s] a) (weaken [relevance s] a') t
b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
- eq2 <- assert_total (doEqual True (cast s') b b')
- pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2))
+ eq2 <- assert_total (doEqual Relevant (cast s') b b')
+ pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
doEqualR Bool (Cnstr Bool) = pure (Cnstr Top)
doEqualR Top (Cnstr Top) = pure (Cnstr Top)
doEqualR Bottom (Cnstr Bottom) = pure (Cnstr Top)
doEqualR a (Cnstr b) = pure (Ntrl $ EqualStuck a b)
export
-doEqualSet : (a, b : NormalForm True ctx) -> LogNormalForm ann True ctx
+doEqualSet : (a, b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
doEqualSet (Ntrl a) b = pure (Ntrl $ EqualL a b)
doEqualSet (Cnstr a) b = doEqualR a b
-doEqual False a t u = pure (Cnstr Top)
-doEqual True (Ntrl a) t u = pure (Ntrl $ Equal a t u)
-doEqual True (Cnstr (Sort Prop)) t u = do
+doEqual Irrelevant a t u = pure (Cnstr Top)
+doEqual Relevant (Ntrl a) t u = pure (Ntrl $ Equal a t u)
+doEqual Relevant (Cnstr (Universe Prop)) t u = do
pure (Cnstr $ Sigma Prop Prop ""
- (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [False] u))
- (Cnstr $ Unsorted.weaken [False] $ Pi Prop Prop "" u (Sorted.weaken [False] t)))
-doEqual True (Cnstr (Sort (Set _))) t u = doEqualSet t u
-doEqual True (Cnstr (Pi s (Set k) var a b)) t u =
- let x : NormalForm (isSet s) (isSet s :: ctx)
+ (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [Irrelevant] u))
+ (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi Prop Prop "" u (Sorted.weaken [Irrelevant] t)))
+doEqual Relevant (Cnstr (Universe (Set _))) t u = doEqualSet t u
+doEqual Relevant (Cnstr (Pi s (Set k) var a b)) t u =
+ let x : NormalForm (relevance s) (relevance s :: ctx)
x = point (var, (s ** Refl)) Here
in do
- t <- assert_total (doApp (weaken [isSet s] t) x)
- u <- assert_total (doApp (weaken [isSet s] u) x)
- eq <- doEqual True b t u
+ t <- assert_total (doApp (weaken [relevance s] t) x)
+ u <- assert_total (doApp (weaken [relevance s] u) x)
+ eq <- doEqual Relevant b t u
pure (Cnstr $ Pi s Prop var a eq)
-doEqual True (Cnstr (Sigma s@(Set _) s' var a b)) t u = do
- t1 <- doFst True (isSet s') t
- u1 <- doFst True (isSet s') u
- t2 <- doSnd True (isSet s') t
- u2 <- doSnd True (isSet s') u
- eq1 <- doEqual True a t1 u1
+doEqual Relevant (Cnstr (Sigma s@(Set _) s' var a b)) t u = do
+ t1 <- doFst Relevant (relevance s') t
+ u1 <- doFst Relevant (relevance s') u
+ t2 <- doSnd Relevant (relevance s') t
+ u2 <- doSnd Relevant (relevance s') u
+ eq1 <- doEqual Relevant a t1 u1
bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure u1) Right))
- t2' <- doCast (isSet s') bt1 bu1 t2
- eq2 <- doEqual (isSet s') (assert_smaller b bu1) t2' u2
- pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [False] eq2))
-doEqual True (Cnstr (Sigma Prop (Set k) var a b)) t u = do
- t2 <- doSnd False True t
- u2 <- doSnd False True u
+ t2' <- doCast (relevance s') bt1 bu1 t2
+ eq2 <- doEqual (relevance s') (assert_smaller b bu1) t2' u2
+ pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [Irrelevant] eq2))
+doEqual Relevant (Cnstr (Sigma Prop (Set k) var a b)) t u = do
+ t2 <- doSnd Irrelevant Relevant t
+ u2 <- doSnd Irrelevant Relevant u
bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
- t2' <- doCast True bt1 bu1 t2
- eq2 <- doEqual True (assert_smaller b bu1) t2' u2
- pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [False] eq2))
-doEqual True (Cnstr Bool) t u = do
- true <- doIf u (Cnstr Top) (Cnstr Bottom)
- false <- doIf u (Cnstr Bottom) (Cnstr Top)
- doIf t true false
-doEqual True (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a
+ t2' <- doCast Relevant bt1 bu1 t2
+ eq2 <- doEqual Relevant (assert_smaller b bu1) t2' u2
+ pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [Irrelevant] eq2))
+doEqual Relevant (Cnstr Bool) t u = do
+ relevant <- doIf u (Cnstr Top) (Cnstr Bottom)
+ irrelevant <- doIf u (Cnstr Bottom) (Cnstr Top)
+ doIf t relevant irrelevant
+doEqual Relevant (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a
substCnstr : Constructor ~|> Hom (LogNormalForm' ann) (LogConstructor ann)
-substCnstr (Sort s) f = pure (Sort s)
+substCnstr (Universe s) f = pure (Universe s)
substCnstr (Pi s s' var a b) f = do
a <- subst' a f
b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f)
@@ -241,26 +244,26 @@ substCnstr False f = pure False
substCnstr Top f = pure Top
substCnstr Bottom f = pure Bottom
-substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann True)
+substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann Relevant)
substNtrl (Var var sort prf i) f = case f i of
Left t => t
Right j => pure (Ntrl $ Var var sort prf j)
-substNtrl (App b t u) f = do
+substNtrl (App r t u) f = do
t <- substNtrl t f
u <- subst' u f
assert_total (doApp t u)
-substNtrl (Fst b t) f = do
+substNtrl (Fst r t) f = do
t <- substNtrl t f
- doFst True b t
-substNtrl (Snd b t) f = do
+ doFst Relevant r t
+substNtrl (Snd r t) f = do
t <- substNtrl t f
- doSnd b True $ rewrite orTrueTrue b in t
+ doSnd r Relevant $ rewrite pairRelevantRight r in t
substNtrl (If t u v) f = do
t <- substNtrl t f
u <- subst' u f
v <- subst' v f
doIf t u v
-substNtrl Absurd f = pure (doAbsurd True)
+substNtrl Absurd f = pure (doAbsurd Relevant)
substNtrl (Equal a t u) f = do
a <- substNtrl a f
t <- subst' t f
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 758b019..f92a0e2 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -4,7 +4,7 @@ import Data.String
import Data.Vect
import Obs.Logging
-import Obs.Sort
+import Obs.Universe
import Obs.Syntax
import System
@@ -299,13 +299,13 @@ parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* m
var : Grammar state ObsToken True (WithBounds Syntax)
var = map (map Var) ident
-noArgSort : Grammar state ObsToken True (WithBounds Sort)
-noArgSort = bounds $
+noArgUniverse : Grammar state ObsToken True (WithBounds Universe)
+noArgUniverse = bounds $
map (const Prop) (match OTProp <* commit) <|>
map (const (Set 0)) (match OTSet <* commit)
-sort : Grammar state ObsToken True (WithBounds Sort)
-sort = bounds $
+universe : Grammar state ObsToken True (WithBounds Universe)
+universe = bounds $
map (const Prop) (match OTProp <* commit) <|>
map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
@@ -326,7 +326,7 @@ lambda p =
[| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
partial
-noSortsTerm : Grammar state ObsToken True (WithBounds Syntax)
+noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax)
partial
term : Grammar state ObsToken True (WithBounds Syntax)
partial
@@ -340,17 +340,17 @@ equals : Grammar state ObsToken True (WithBounds Syntax)
partial
exp : Grammar state ObsToken True (WithBounds Syntax)
-noSortsTerm =
+noUniversesTerm =
parens exp <|>
var <|>
bounds (map (uncurry Pair) (pair exp)) <|>
bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
-term = noSortsTerm <|> map (map Sort) noArgSort
+term = noUniversesTerm <|> map (map Universe) noArgUniverse
head =
- noSortsTerm <|>
- map (map Sort) sort <|>
+ noUniversesTerm <|>
+ map (map Universe) universe <|>
bounds
(choiceMap
(\(hd, (n ** f)) => match hd *> commit *>
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
deleted file mode 100644
index 4e0e9c9..0000000
--- a/src/Obs/Sort.idr
+++ /dev/null
@@ -1,110 +0,0 @@
-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
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 7bf4b61..32e86c0 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -1,7 +1,7 @@
||| Raw syntax for terms. This is before eliminating names.
module Obs.Syntax
-import Obs.Sort
+import Obs.Universe
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
@@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter
public export
data Syntax : Type where
Var : String -> Syntax
- -- Sorts
- Sort : Sort -> Syntax
+ -- Universes
+ Universe : Universe -> Syntax
-- Dependent Products
Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
Lambda : WithBounds String -> WithBounds Syntax -> Syntax
@@ -55,7 +55,7 @@ prettyPrec : Prec -> Syntax -> Doc ann
prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
prettyPrec d (Var var) = pretty var
-prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Universe s) = prettyPrec d s
prettyPrec d (Pi var a b) =
parenthesise (d > Open) $
group $
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 422af87..c4d9e40 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -2,7 +2,7 @@
module Obs.Term
import Data.Fin
-import Obs.Sort
+import Obs.Universe
import Text.Bounded
import Text.PrettyPrint.Prettyprinter
@@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter
public export
data Term : Nat -> Type where
Var : String -> Fin n -> Term n
- -- Sorts
- Sort : Sort -> Term n
+ -- Universes
+ Universe : Universe -> Term n
-- Dependent Product
Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
@@ -74,7 +74,7 @@ prettyPrec : Prec -> Term n -> Doc ann
prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
prettyPrec d (Var var _) = pretty var
-prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Universe s) = prettyPrec d s
prettyPrec d (Pi var a b) =
parenthesise (d > Open) $
group $
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 4cc6d8e..7bb5deb 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -9,11 +9,11 @@ import Decidable.Equality
import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
-import Obs.Sort
import Obs.Substitution
import Obs.Term
import Obs.Typing.Context
import Obs.Typing.Conversion
+import Obs.Universe
import System
@@ -33,44 +33,44 @@ mismatch lhs rhs = fatal $
typeMismatch : Doc ann -> Doc ann -> Logging ann a
typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs
-sortMismatch : Doc ann -> Doc ann -> Logging ann a
-sortMismatch lhs rhs = inScope "sort mismatch" $ mismatch lhs rhs
+universeMismatch : Doc ann -> Doc ann -> Logging ann a
+universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
-- Utilities -------------------------------------------------------------------
-MkPair : (s, s' : Sort)
- -> NormalForm (isSet s) ctx
- -> NormalForm (isSet s') ctx
- -> NormalForm (isSet (max s s')) ctx
+MkPair : (s, s' : Universe)
+ -> NormalForm (relevance s) ctx
+ -> NormalForm (relevance s') ctx
+ -> NormalForm (relevance (max s s')) ctx
MkPair Prop Prop t u = u
-MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Oh t u
-MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Oh t u
+MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Set t u
+MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u
-- Checking and Inference ------------------------------------------------------
check : (tyCtx : TyContext ctx)
- -> (s : Sort)
- -> NormalForm True ctx
+ -> (s : Universe)
+ -> TypeNormalForm ctx
-> WithBounds (Term (length ctx))
- -> Logging ann (NormalForm (isSet s) ctx)
+ -> Logging ann (NormalForm (relevance s) ctx)
checkType : (tyCtx : TyContext ctx)
- -> (s : Sort)
+ -> (s : Universe)
-> WithBounds (Term (length ctx))
- -> Logging ann (NormalForm True ctx)
-checkType ctx s tm = check ctx (suc s) (cast s) tm
+ -> Logging ann (TypeNormalForm ctx)
+checkType ctx s tm = check ctx (succ s) (cast s) tm
infer : (tyCtx : TyContext ctx)
-> WithBounds (Term (length ctx))
- -> Logging ann (s ** (NormalForm True ctx, NormalForm (isSet s) ctx))
+ -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
-> (tyCtx : TyContext ctx)
-> WithBounds (Term (length ctx))
- -> Logging ann (Sort, NormalForm True ctx)
+ -> Logging ann (Universe, TypeNormalForm ctx)
inferType ctx tm = inBounds tm.bounds $ do
- (Set _ ** (Cnstr (Sort s), a)) <- infer ctx tm
- | (_ ** (a, t)) => tag (pretty "sort") (pretty a)
+ (Set _ ** (Cnstr (Universe s), a)) <- infer ctx tm
+ | (_ ** (a, t)) => tag (pretty "universe") (pretty a)
pure (s, a)
check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
@@ -79,7 +79,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
trace $ pretty {ann} "checking body has type" <++> pretty b
t <- check (ctx ::< MkFreeVar l a var.val) l' b (assert_smaller tm t)
let Yes Refl = decEq s (l ~> l')
- | No _ => fatal "internal sort mismatch"
+ | No _ => fatal "internal universe mismatch"
pure $ case l' of
Prop => Irrel
Set _ => Cnstr (Lambda l var.val t)
@@ -92,7 +92,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
trace $ pretty {ann} "checking second has type" <++> pretty b
u <- check ctx l' b (assert_smaller tm u)
let Yes Refl = decEq s (max l l')
- | No _ => fatal "internal sort mismatch"
+ | No _ => fatal "internal universe mismatch"
pure $ MkPair l l' t u
(_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty)
(_, Absurd t) => do
@@ -108,7 +108,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
| No _ => typeMismatch (pretty a) (pretty b)
a' <- subst a (reduce ctx)
b' <- subst b (reduce ctx)
- Just _ <- inScope "convert" $ runMaybeT $ convert (suc s) (cast s) a' b'
+ Just _ <- inScope "convert" $ runMaybeT $ convert (succ s) (cast s) a' b'
| Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b)
pure t
@@ -117,16 +117,16 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
info $ pretty {ann} "encountered variable" <++> pretty tm.val
let def = index' ctx i
pure (def.sort ** (def.ty, def.tm))
- (Sort s) => do
- info $ pretty {ann} "encountered sort" <++> pretty tm.val
- pure (suc (suc s) ** (cast (suc s), cast s))
+ (Universe s) => do
+ info $ pretty {ann} "encountered universe" <++> pretty tm.val
+ pure (succ (succ s) ** (cast (succ s), cast s))
(Pi var a b) => do
info "encountered pi"
(s, a) <- inferType ctx (assert_smaller tm a)
trace $ pretty {ann} "domain type is" <++> pretty a
(s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
trace $ pretty {ann} "codomain type is" <++> pretty b
- pure (suc (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b)))
+ pure (succ (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b)))
(Lambda var t) => fatal "cannot infer type of lambda"
(App t u) => do
info "encountered application"
@@ -137,17 +137,17 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
u <- check ctx l a (assert_smaller tm u)
trace $ pretty {ann} "argument is well typed"
let Yes Refl = decEq s (l ~> l')
- | No _ => fatal "internal sort mismatch"
+ | No _ => fatal "internal universe mismatch"
ty <- subst1 u b
tm <- doApp t u
- pure (l' ** (ty, rewrite sym $ impredicative l l' in tm))
+ pure (l' ** (ty, rewrite sym $ functionRelevance l l' in tm))
(Sigma var a b) => do
info "encountered sigma"
(s, a) <- inferType ctx (assert_smaller tm a)
trace $ pretty {ann} "first type is" <++> pretty a
(s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
trace $ pretty {ann} "second type is" <++> pretty b
- pure (suc (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b)))
+ pure (succ (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b)))
(Pair t u) => fatal "cannot infer type of pair"
(Fst t) => do
info "encountered first"
@@ -155,9 +155,9 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
| (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
trace $ pretty {ann} "pair has type" <++> pretty ty
let Yes Refl = decEq s (max l l')
- | No _ => fatal "internal sort mismatch"
+ | No _ => fatal "internal universe mismatch"
let ty = a
- tm <- doFst (isSet l) (isSet l') (rewrite sym $ maxIsSet l l' in t)
+ tm <- doFst (relevance l) (relevance l') (rewrite sym $ pairRelevance l l' in t)
pure (l ** (ty, tm))
(Snd t) => do
info "encountered second"
@@ -165,11 +165,11 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
| (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
trace $ pretty {ann} "pair has type" <++> pretty ty
let Yes Refl = decEq s (max l l')
- | No _ => fatal "internal sort mismatch"
- let t = rewrite sym $ maxIsSet l l' in t
- fst <- doFst (isSet l) (isSet l') t
+ | No _ => fatal "internal universe mismatch"
+ let t = rewrite sym $ pairRelevance l l' in t
+ fst <- doFst (relevance l) (relevance l') t
ty <- subst1 fst b
- tm <- doSnd (isSet l) (isSet l') t
+ tm <- doSnd (relevance l) (relevance l') t
pure (l' ** (ty, tm))
Bool => do
info "encountered bool"
@@ -197,13 +197,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
pure (s ** (ty, tm))
Top => do
info "encountered top"
- pure (Set 0 ** (cast Prop, Cnstr Top))
+ pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Top))
Point => do
info "encountered point"
pure (Prop ** (Cnstr Top, Irrel))
Bottom => do
info "encountered bottom"
- pure (Set 0 ** (cast Prop, Cnstr Bottom))
+ pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Bottom))
(Absurd t) => fatal "cannot infer type of absurd"
(Equal t u) => do
info "encountered equal"
@@ -211,13 +211,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
trace $ pretty {ann} "left side has type" <++> pretty a
u <- check ctx s a (assert_smaller tm u)
trace "right side is well typed"
- eq <- doEqual (isSet s) a t u
- pure (Set 0 ** (cast Prop, eq))
+ eq <- doEqual (relevance s) a t u
+ pure (Set 0 ** (Cnstr (Universe Prop), eq))
(Refl t) => do
info "encountered refl"
(s ** (a, t)) <- infer ctx (assert_smaller tm t)
trace "argument is well typed"
- eq <- doEqual (isSet s) a t t
+ eq <- doEqual (relevance s) a t t
pure (Prop ** (eq, Irrel))
(Transp b t u t' e) => do
info "encountered transp"
@@ -225,12 +225,12 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
trace $ pretty {ann} "index type is" <++> pretty a
t' <- check ctx s a (assert_smaller tm t')
trace "new index is well typed"
- b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (cast Prop)) (assert_smaller tm b)
+ b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (Cnstr (Universe Prop))) (assert_smaller tm b)
trace "transporting in Prop"
oldB <- doApp b t
u <- check ctx Prop oldB (assert_smaller tm u)
trace "old-indexed proposition is well typed"
- eq <- doEqual (isSet s) a t t'
+ eq <- doEqual (relevance s) a t t'
trace $ pretty {ann} "checking equality has type" <++> pretty eq
e <- check ctx Prop eq (assert_smaller tm e)
trace "equality is well typed"
@@ -242,19 +242,19 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
trace $ pretty {ann} "old type is" <++> pretty a
b <- checkType ctx s (assert_smaller tm b)
trace $ pretty {ann} "new type is" <++> pretty b
- eq <- doEqual True (cast s) a b
+ eq <- doEqual Relevant (cast s) a b
e <- check ctx Prop eq (assert_smaller tm e)
trace "equality is well typed"
t <- check ctx s a (assert_smaller tm t)
trace "value is well typed"
- tm <- doCast (isSet s) a b t
+ tm <- doCast (relevance s) a b t
pure (s ** (b, tm))
(CastId t) => do
info "encountered castRefl"
(s ** (a, t)) <- infer ctx (assert_smaller tm t)
trace $ pretty {ann} "argument has type" <++> pretty a
- lhs <- doCast (isSet s) a a t
- ret <- doEqual (isSet s) a lhs t
+ lhs <- doCast (relevance s) a a t
+ ret <- doEqual (relevance s) a lhs t
pure (Prop ** (ret, Irrel))
-- Checking Definitions and Blocks ---------------------------------------------
diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
index 636c9f2..4706dca 100644
--- a/src/Obs/Typing/Context.idr
+++ b/src/Obs/Typing/Context.idr
@@ -8,7 +8,7 @@ import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
import Obs.Substitution
-import Obs.Sort
+import Obs.Universe
import Text.Bounded
@@ -17,40 +17,40 @@ import Text.Bounded
infix 5 ::<
public export
-record FreeVar (ctx : List Bool) where
+record FreeVar (ctx : List Relevance) where
constructor MkFreeVar
- sort : Sort
- ty : NormalForm True ctx
+ sort : Universe
+ ty : TypeNormalForm ctx
name : String
public export
-record TyDef (b : Bool) (ctx : List Bool) where
+record TyDef (b : Relevance) (ctx : List Relevance) where
constructor MkDefinition
name : String
- sort : Sort
- ty : NormalForm True ctx
- tm : NormalForm (isSet sort) ctx
- correct : isSet sort = b
+ sort : Universe
+ ty : TypeNormalForm ctx
+ tm : NormalForm (relevance sort) ctx
+ correct : relevance sort = b
public export
-data TyContext : Unsorted.Family Bool where
+data TyContext : Unsorted.Family Relevance where
Nil : TyContext []
- (:<) : TyContext ctx -> (def : Definition ctx) -> TyContext (isSet def.sort :: ctx)
- (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (isSet var.sort :: ctx)
+ (:<) : TyContext ctx -> (def : Definition ctx) -> TyContext (relevance def.sort :: ctx)
+ (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (relevance var.sort :: ctx)
-- Properties ------------------------------------------------------------------
-freeVars : TyContext ctx -> List Bool
+freeVars : TyContext ctx -> List Relevance
freeVars [] = []
freeVars (ctx :< def) = freeVars ctx
-freeVars (ctx ::< var) = isSet var.sort :: freeVars ctx
+freeVars (ctx ::< var) = relevance var.sort :: freeVars ctx
-Sorted.Rename Bool TyDef where
+Sorted.Rename Relevance TyDef where
rename def f = {ty := rename def.ty f, tm := rename def.tm f} def
-- Construction ----------------------------------------------------------------
-fromDef : (def : Definition ctx) -> TyDef (isSet def.sort) ctx
+fromDef : (def : Definition ctx) -> TyDef (relevance def.sort) ctx
fromDef def = MkDefinition
{ name = def.name.val
, sort = def.sort
@@ -59,11 +59,11 @@ fromDef def = MkDefinition
, correct = Refl
}
-fromVar : (var : FreeVar ctx) -> TyDef (isSet var.sort) (isSet var.sort :: ctx)
+fromVar : (var : FreeVar ctx) -> TyDef (relevance var.sort) (relevance var.sort :: ctx)
fromVar var = MkDefinition
{ name = var.name
, sort = var.sort
- , ty = weaken [isSet var.sort] var.ty
+ , ty = weaken [relevance var.sort] var.ty
, tm = point (var.name, (var.sort ** Refl)) Here
, correct = Refl
}
@@ -80,10 +80,10 @@ getContext : TyContext ctx -> (ctx' ** ctx = ctx')
getContext [] = ([] ** Refl)
getContext (ctx :< def) =
let (ctx' ** prf) = getContext ctx in
- (isSet def.sort :: ctx' ** cong (isSet def.sort ::) prf)
+ (relevance def.sort :: ctx' ** cong (relevance def.sort ::) prf)
getContext (ctx ::< var) =
let (ctx' ** prf) = getContext ctx in
- (isSet var.sort :: ctx' ** cong (isSet var.sort ::) prf)
+ (relevance var.sort :: ctx' ** cong (relevance var.sort ::) prf)
export
index : TyContext ctx -> Map ctx TyDef ctx
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index d5dc86a..766c21e 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -4,36 +4,36 @@ import Control.Monad.Maybe
import Control.Monad.Trans
import Data.Bool
-import Data.So
+import Data.Nat
import Decidable.Equality
import Obs.Logging
import Obs.NormalForm
import Obs.NormalForm.Normalise
-import Obs.Sort
import Obs.Substitution
+import Obs.Universe
%default total
-- Conversion ------------------------------------------------------------------
export
-convert : (s : Sort)
- -> (a : NormalForm True ctx)
- -> (t, u : NormalForm (isSet s) ctx)
- -> MaybeT (Logging ann) (NormalForm (isSet s) ctx)
+convert : (s : Universe)
+ -> (a : TypeNormalForm ctx)
+ -> (t, u : NormalForm (relevance s) ctx)
+ -> MaybeT (Logging ann) (NormalForm (relevance s) ctx)
-untypedConvert : (t, u : NormalForm True ctx) -> MaybeT (Logging ann) (NormalForm True ctx)
+untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx)
-- Diagonals
-untypedConvert (Cnstr (Sort s)) (Cnstr (Sort s')) =
- if s == s' then pure (Cnstr (Sort s)) else nothing
+untypedConvert (Cnstr (Universe s)) (Cnstr (Universe s')) =
+ if s == s' then pure (Cnstr (Universe s)) else nothing
untypedConvert (Cnstr (Pi s s' var a b)) (Cnstr (Pi l l' _ a' b')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "going back to type-directed conversion"
- a <- assert_total (convert (suc s) (cast s) a a')
- b <- assert_total (convert (suc s') (cast s') b b')
+ a <- assert_total (convert (succ s) (cast s) a a')
+ b <- assert_total (convert (succ s') (cast s') b b')
pure (Cnstr $ Pi s s' var a b)
untypedConvert (Cnstr (Lambda s var t)) (Cnstr (Lambda s' _ u)) = do
let Yes Refl = decEq s s'
@@ -45,8 +45,8 @@ untypedConvert (Cnstr (Sigma s s' var a b)) (Cnstr (Sigma l l' _ a' b')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "going back to type-directed conversion"
- a <- assert_total (convert (suc s) (cast s) a a')
- b <- assert_total (convert (suc s') (cast s') b b')
+ a <- assert_total (convert (succ s) (cast s) a a')
+ b <- assert_total (convert (succ s') (cast s') b b')
pure (Cnstr $ Sigma s s' var a b)
untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf' t' u')) = do
let Yes Refl = decEq (s, s') (l, l')
@@ -54,19 +54,19 @@ untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf
lift $ trace "converting pair pointwise"
t <- untypedConvert t t'
u <- untypedConvert u u'
- pure (Cnstr $ Pair l l' Oh t u)
+ pure (Cnstr $ Pair l l' Set t u)
untypedConvert (Cnstr (Pair s@(Set _) Prop prf t u)) (Cnstr (Pair l Prop prf' t' u')) = do
let Yes Refl = decEq s l
| No _ => nothing
lift $ trace "converting pair pointwise"
t <- untypedConvert t t'
- pure (Cnstr $ Pair l Prop Oh t Irrel)
+ pure (Cnstr $ Pair l Prop Set t Irrel)
untypedConvert (Cnstr (Pair Prop s'@(Set _) prf t u)) (Cnstr (Pair Prop l' prf' t' u')) = do
let Yes Refl = decEq s' l'
| No _ => nothing
lift $ trace "converting pair pointwise"
u <- untypedConvert u u'
- pure (Cnstr $ Pair Prop l' Oh Irrel u)
+ pure (Cnstr $ Pair Prop l' Set Irrel u)
untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
@@ -74,23 +74,23 @@ untypedConvert (Cnstr Top) (Cnstr Top) = pure (Cnstr Top)
untypedConvert (Cnstr Bottom) (Cnstr Bottom) = pure (Cnstr Bottom)
untypedConvert t@(Ntrl (Var _ _ _ i)) (Ntrl (Var _ _ _ j)) =
if elemToNat i == elemToNat j then pure t else nothing
-untypedConvert lhs@(Ntrl (App b t u)) rhs@(Ntrl (App b' t' u')) = do
- let Yes Refl = decEq b b'
+untypedConvert lhs@(Ntrl (App r t u)) rhs@(Ntrl (App r' t' u')) = do
+ let Yes Refl = decEq r r'
| No _ => nothing
lift $ trace "checking parts of a spine"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
- let True = b'
- | False => lift $ doApp t Irrel
+ let Relevant = r'
+ | Irrelevant => lift $ doApp t Irrel
u <- untypedConvert u u'
lift $ doApp t u
-untypedConvert lhs@(Ntrl (Fst b t)) rhs@(Ntrl (Fst b' t')) = do
+untypedConvert lhs@(Ntrl (Fst r t)) rhs@(Ntrl (Fst r' t')) = do
lift $ trace "checking full pair for fst"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
- lift $ doFst True b t
-untypedConvert lhs@(Ntrl (Snd b t)) rhs@(Ntrl (Snd b' t')) = do
+ lift $ doFst Relevant r t
+untypedConvert lhs@(Ntrl (Snd r t)) rhs@(Ntrl (Snd r' t')) = do
lift $ trace "checking full pair for snd"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
- lift $ doSnd b True (rewrite orTrueTrue b in t)
+ lift $ doSnd r Relevant (rewrite pairRelevantRight r in t)
untypedConvert lhs@(Ntrl (If t f g)) rhs@(Ntrl (If t' f' g')) = do
lift $ trace "checking all branches of if"
t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
@@ -139,25 +139,25 @@ untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do
lift $ doCast _ a b t
-- Pi types
untypedConvert t@(Cnstr (Lambda s var _)) (Ntrl u) = do
- u <- lift $ doApp (Ntrl $ weaken [isSet s] u) (point (var, (s ** Refl)) Here)
+ u <- lift $ doApp (Ntrl $ weaken [relevance s] u) (point (var, (s ** Refl)) Here)
assert_total (untypedConvert t (Cnstr (Lambda s var u)))
untypedConvert (Ntrl t) u@(Cnstr (Lambda s var _)) = do
- t <- lift $ doApp (Ntrl $ weaken [isSet s] t) (point (var, (s ** Refl)) Here)
+ t <- lift $ doApp (Ntrl $ weaken [relevance s] t) (point (var, (s ** Refl)) Here)
assert_total (untypedConvert (Cnstr (Lambda s var t)) u)
-- Sigma types
untypedConvert t@(Cnstr (Pair s s' prf _ _)) t'@(Ntrl _) =
- let t'' : NormalForm (isSet s || isSet s') ctx
- t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t'
+ let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
+ t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t'
in do
- t' <- lift $ doFst (isSet s) (isSet s') t''
- u' <- lift $ doSnd (isSet s) (isSet s') t''
+ t' <- lift $ doFst (relevance s) (relevance s') t''
+ u' <- lift $ doSnd (relevance s) (relevance s') t''
assert_total (untypedConvert t (Cnstr (Pair s s' prf t' u')))
untypedConvert t@(Ntrl _) t'@(Cnstr (Pair s s' prf _ _)) =
- let t'' : NormalForm (isSet s || isSet s') ctx
- t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t
+ let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
+ t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t
in do
- t <- lift $ doFst (isSet s) (isSet s') t''
- u <- lift $ doSnd (isSet s) (isSet s') t''
+ t <- lift $ doFst (relevance s) (relevance s') t''
+ u <- lift $ doSnd (relevance s) (relevance s') t''
assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
-- Bools
-- no cases because diagonals complete
@@ -168,33 +168,33 @@ convert Prop a Irrel Irrel = pure Irrel
convert (Set k) (Ntrl a) t u = do
lift $ trace $ pretty {ann} "cannot do type-directed conversion on" <++> pretty a
untypedConvert t u
-convert (Set k) (Cnstr (Sort s)) t u = do
+convert (Set k) (Cnstr (Universe s)) t u = do
lift $ trace $ pretty {ann} "converting in type" <++> pretty s
untypedConvert t u
convert (Set k) (Cnstr (Pi s s'@(Set _) var a b)) t u = do
-- s' must be Set, otherwise ty is in Prop
lift $ trace "converting pi type"
- t' <- lift $ doApp (Sorted.weaken [isSet s] t) (point (var, (s ** Refl)) Here)
- u' <- lift $ doApp (Sorted.weaken [isSet s] u) (point (var, (s ** Refl)) Here)
+ t' <- lift $ doApp (Sorted.weaken [relevance s] t) (point (var, (s ** Refl)) Here)
+ u' <- lift $ doApp (Sorted.weaken [relevance s] u) (point (var, (s ** Refl)) Here)
t <- convert s' b t' u'
pure (Cnstr $ Lambda s var t)
convert (Set k) ty@(Cnstr (Sigma s@(Set j) s' var a b)) t u = do
lift $ trace "converting sigma type"
- t1 <- lift $ doFst True (isSet s') t
- u1 <- lift $ doFst True (isSet s') u
+ t1 <- lift $ doFst Relevant (relevance s') t
+ u1 <- lift $ doFst Relevant (relevance s') u
t1 <- convert s a t1 u1
- t2 <- lift $ doSnd True (isSet s') t
- u2 <- lift $ doSnd True (isSet s') u
+ t2 <- lift $ doSnd Relevant (relevance s') t
+ u2 <- lift $ doSnd Relevant (relevance s') u
b <- lift $ subst1 t1 b
t2 <- convert s' (assert_smaller ty b) t2 u2
- pure (Cnstr $ Pair s s' Oh t1 t2)
+ pure (Cnstr $ Pair s s' Set t1 t2)
convert (Set k) ty@(Cnstr (Sigma Prop s'@(Set _) var a b)) t u = do
lift $ trace "converting sigma type (snd only)"
- t2 <- lift $ doSnd False True t
- u2 <- lift $ doSnd False True u
+ t2 <- lift $ doSnd Irrelevant Relevant t
+ u2 <- lift $ doSnd Irrelevant Relevant u
b <- lift $ subst1 Irrel b
t2 <- convert s' (assert_smaller ty b) t2 u2
- pure (Cnstr $ Pair Prop s' Oh Irrel t2)
+ pure (Cnstr $ Pair Prop s' Set Irrel t2)
convert (Set 0) (Cnstr Bool) (Cnstr True) (Cnstr True) = do
lift $ trace "converting bool (true)"
pure (Cnstr True)
diff --git a/src/Obs/Universe.idr b/src/Obs/Universe.idr
new file mode 100644
index 0000000..1517c4c
--- /dev/null
+++ b/src/Obs/Universe.idr
@@ -0,0 +1,222 @@
+||| 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
+
+||| True if values in `s` are proof-irrelevant.
+public export
+isIrrelevant : (s : Universe) -> Bool
+isIrrelevant = (Irrelevant ==) . relevance
+
+||| True if values in `s` are proof-relevant.
+public export
+isRelevant : (s : Universe) -> Bool
+isRelevant = (Relevant ==) . relevance
+
+||| 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 : Universe -> Type where
+ Prop : IsIrrelevant Prop
+
+ public export
+ data IsRelevant : Universe -> Type where
+ Set : IsRelevant (Set k)
+
+ export
+ Uninhabited (IsIrrelevant (Set k)) where
+ uninhabited _ impossible
+
+ export
+ Uninhabited (IsRelevant Prop) where
+ uninhabited _ impossible
+
+ export
+ isIrrelevant : (s : Universe) -> Dec (IsIrrelevant s)
+ isIrrelevant Prop = Yes Prop
+ isIrrelevant (Set k) = No absurd
+
+ export
+ isRelevant : (s : Universe) -> Dec (IsRelevant s)
+ isRelevant Prop = No absurd
+ isRelevant (Set k) = Yes Set
+
+-- 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
+
+irrelevantReflection : (s : Universe) -> Reflects (IsIrrelevant s) (isIrrelevant s)
+irrelevantReflection Prop = RTrue Prop
+irrelevantReflection (Set k) = RFalse absurd
+
+relevantReflection : (s : Universe) -> Reflects (IsRelevant s) (isRelevant s)
+relevantReflection Prop = RFalse absurd
+relevantReflection (Set k) = RTrue Set
+
+export
+forgetIsIrrelevant : IsIrrelevant s -> relevance s = Irrelevant
+forgetIsIrrelevant Prop = Refl
+
+export
+forgetIsRelevant : IsRelevant s -> relevance s = Relevant
+forgetIsRelevant Set = Refl
+
+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
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 08:57:03 +0000