Add more program structure to normal forms.

1 files changed, 12 insertions, 38 deletions

diff --git a/src/Obs/Universe.idr b/src/Obs/Universe.idr
index 1517c4c..14cde14 100644
--- a/src/Obs/Universe.idr
+++ b/src/Obs/Universe.idr
@@ -127,16 +127,6 @@ 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
@@ -155,30 +145,30 @@ dom ~> (Set k) = max (Set k) dom
 
 namespace Predicates
   public export
-  data IsIrrelevant : Universe -> Type where
-    Prop : IsIrrelevant Prop
+  data IsIrrelevant : Relevance -> Type where
+    Irrelevant : IsIrrelevant Irrelevant
 
   public export
-  data IsRelevant : Universe -> Type where
-    Set : IsRelevant (Set k)
+  data IsRelevant : Relevance -> Type where
+    Relevant : IsRelevant Relevant
 
   export
-  Uninhabited (IsIrrelevant (Set k)) where
+  Uninhabited (IsIrrelevant Relevant) where
     uninhabited _ impossible
 
   export
-  Uninhabited (IsRelevant Prop) where
+  Uninhabited (IsRelevant Irrelevant) where
     uninhabited _ impossible
 
   export
-  isIrrelevant : (s : Universe) -> Dec (IsIrrelevant s)
-  isIrrelevant Prop = Yes Prop
-  isIrrelevant (Set k) = No absurd
+  isIrrelevant : (r : Relevance) -> Dec (IsIrrelevant r)
+  isIrrelevant Irrelevant = Yes Irrelevant
+  isIrrelevant Relevant = No absurd
 
   export
-  isRelevant : (s : Universe) -> Dec (IsRelevant s)
-  isRelevant Prop = No absurd
-  isRelevant (Set k) = Yes Set
+  isRelevant : (r : Relevance) -> Dec (IsRelevant r)
+  isRelevant Irrelevant = No absurd
+  isRelevant Relevant = Yes Relevant
 
 -- Properties ------------------------------------------------------------------
 
@@ -194,22 +184,6 @@ 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