Commit 31ad24af authored by Gaspard Ferey's avatar Gaspard Ferey

Merge branch 'master' of git.lsv.fr:genestier/PleinDeDk

parents 7c71d534 31a7ac60
(; cast, WIP, varity ;)
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z (s j) --> s j.
[i,j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[] rule _ prop --> prop.
[i] rule prop (type i) --> type i.
[i,j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[] sup prop prop --> prop.
[i] sup prop (type i) --> type i.
[i] sup (type i) prop --> type i.
[i,j] sup (type i) (type j) --> type (max i j).
(; Canonicity rules ;)
[s1] sup s1 s1 --> s1.
[s1,s2] succ (sup s1 s2) --> sup (succ s1) (succ s2).
[s1,s2,s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1,s2,s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (sup s1 s2) s3 --> sup (rule s1 s3) (rule s2 s3).
(; Primitive ;)
U : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
u : s : Sort -> U (succ s).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
def join : s1 : Sort -> s2 : Sort -> U s1 -> U s2 -> U (sup s1 s2).
def cast : s1 : Sort -> s2 : Sort -> a : U s1 -> b : U s2 -> T s1 a -> T (sup s1 s2) (join s1 s2 a b).
(; Defining code interpretation: T ;)
[s] T _ (u s) --> U s.
[s,a] T _ (cast _ _ (u s) _ a) --> T s a.
[s1,s2,a,b] T _ (prod s1 s2 a b) --> x : T s1 a -> T s2 (b x).
(; Defining join ;)
[i] join _ _ i i --> i.
[s1,s2] join _ _ (u s1) (u s2) --> u (sup s1 s2).
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod s1 s3 a c)
--> prod s1 (sup s2 s3) a (x : T s1 a => join s2 s3 (b x) (c x)).
(; Defining cast ;)
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3, m : T s1 a];)
(;cast {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b) m;)
(;--> cast s1 s3 a b m.;)
[s1,s2,s3,a,b,c,m,x]
cast _ _ (prod s1 s2 a b) (prod s1 s3 a c) m x
--> cast s2 s3 (b x) (c x) (m x).
(; Canonicity rules ;)
[t,a] cast _ _ t t a --> a.
[s1,s2,s3,a]
cast (succ (sup s1 s2)) (succ s3) (u (sup s1 s2)) (u s3) (cast (succ s1) (succ s2) (u s1) (u s2) a)
--> cast (succ s1) (succ (sup s2 s3)) (u s1) (u (sup s2 s3)) a.
[s1,s2,s3,a,b]
prod _ s2 (cast _ _ (u s1) (u s3) a) (x => b x)
--> cast
(succ (rule s1 s2))
(succ (rule s3 s2))
(u (rule s1 s2))
(u (rule s3 s2))
(prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => cast _ _ (u s2) (u s3) (b x))
--> cast
(succ (rule s1 s2))
(succ (rule s1 s3))
(u (rule s1 s2))
(u (rule s1 s3))
(prod s1 s2 a (x => b x)).
(; Alias for universe casting: lift ;)
def lift : s1 : Sort -> s2 : Sort -> U s1 -> U (sup s1 s2).
[s1,s2,m] lift s1 s2 m --> cast (succ s1) (succ s2) (u s1) (u s2) m.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment