Commit 332a7d9b authored by Francois THIRE's avatar Francois THIRE

Add two theories

parent 6eb956d4
#NAME stt.
type : Type.
prop : type.
arrow : type -> type -> type.
def eta : type -> Type.
forall : A:type -> (eta A -> eta prop) -> eta prop.
impl : eta prop -> eta prop -> eta prop.
def eps : eta prop -> Type.
[a, b] eta (arrow a b) --> eta a -> eta b.
[A, f] eps (forall A f) --> x:eta A -> eps (f x).
[l, r] eps (impl l r) --> eps l -> eps r.
(; Full polymorphism makes this theory inconsistent ;)
forall_kind_type : (type -> type) -> type.
[f] eta (forall_kind_type f) --> x:type -> eta (f x).
forall_kind_prop : (type -> eta prop) -> eta prop.
[f] eps (forall_kind_prop f) --> x:type -> eps (f x).
\ No newline at end of file
#NAME sttforall.
type : Type.
arr : type -> type -> type.
bool : type.
def eta : type -> Type.
ptype : Type.
p : type -> ptype.
def etap : ptype -> Type.
forallK : (type -> ptype) -> ptype.
def eps : eta bool -> Type.
impl : eta bool -> eta bool -> eta bool.
forall : t:type -> (eta t -> eta bool) -> eta bool.
forallP : (type -> eta bool) -> eta bool.
[] eta --> t => etap (p t).
[l,r] etap (p (arr l r)) --> eta l -> eta r.
[f] etap (forallK f) --> x : type -> etap (f x).
[t,f] eps (forall t f) --> x:eta t -> eps (f x).
[l,r] eps (impl l r) --> eps l -> eps r.
[f] eps (forallP f) --> x:type -> eps (f x).
def leibniz : etap (forallK (X:type => p (arr X (arr X bool)))) :=
X:type =>
x:eta X =>
y:eta X =>
forall (arr X bool) (P => impl (P x) (P y)).
def refl : eps (forallP (X => forall X (x:eta X => leibniz X x x))) :=
X:type =>
x:eta X =>
P:eta (arr X bool) =>
p:eps (P x) => p.
\ No newline at end of file
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