From 74f0dc953839179aae071dda1ddb924295bc6061 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 2 Jan 2023 15:43:24 +0000 Subject: Add more program structure to type universes. --- src/Obs/Universe.idr | 222 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 222 insertions(+) create mode 100644 src/Obs/Universe.idr (limited to 'src/Obs/Universe.idr') 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 -- cgit v1.2.3