Delta-Lambda-0.3.0.0: library/stdlib.dl

-- the base term of stdlib is an embedding of first order intuitionistic logic
[

-- we need a method of transforming statements in our embedding into others.
-- delta lambda can encode most type systems using the 'judgments as types'
-- principal, however it does get difficult to handle equality Judgements
-- between terms. below is my attempt to deal with this difficulty

equals : [x: type, X, Y: x] type,
reflexivity : [x: type, :x] (x, x) equals,
symmetry : [x, y: type, :(x, y) equals] (y, x) equals,
transitivity : [x, y, z: type, :(x, y) equals, :(y, z) equals] (x, z) equals

-- prop is the type of proposition, set the type of data/sets
prop, set : type,

-- now for the rules of the types under prop
true, false: prop,
and, or, implies, is : [:prop, :prop] prop,
not : [:prop] false,

-- here's the inhabitants (aka proofs) for the above type formations
TRUE: true,
pair : [x, y: prop, :x, :y] : (x, y) and,
left : [x, y: prop, :x] : (x, y) or,
right : [x, y: prop, :y] : (x, y) or,
funct : [x, y: prop, : [: x] y ] (x, y) implies,
path : [x: prop] (x, x) is,


-- this is how we transform (aka reduce) from one proof to another
first : [x, y: prop, :(x, y) and] x,
second : [x, y: prop, :(x, y) and] y,
case : [x, y, z: prop, :(x, y) or, :[:x] z, :[:y] z ] z,
call : [x, y: prop, :(x, y) implies, :x] y,
follow : [x, y: prop, :(x, y) is, :[:x] prop] [:y] prop,
ex_falso : [:false, :prop] prop

-- the rules for equality between terms are where the complexity arises

] type