\* Intuitionistic Predicate Logic with Equality *\
-\open elements \* [1] 2.1. 2.2. *\
+\open elements \* [1] 2.1. 2.2. 3.1 *\
\decl "logical false" False: *Prop
\def "logical implication"
Imp = [p:*Prop, q:*Prop] p -> q : *Prop => *Prop -> *Prop
- \decl "logical comprehension" All: (*Obj -> *Prop) -> *Prop
+\* comprehension and dependent abstraction are isomorphic *\
+ \def "unrestricted logical comprehension"
+ All = [q:*Obj->*Prop] [x:*Obj] q(x) : (*Obj -> *Prop) -> *Prop
- \decl "logical existence" Ex: (*Obj -> *Prop) -> *Prop
+ \decl "unrestricted logical existence" Ex: (*Obj -> *Prop) -> *Prop
\decl "syntactical identity" Id: *Obj => *Obj -> *Prop
\def "logical equivalence"
Iff = [p:*Prop, q:*Prop] And(p -> q, q -> p) : *Prop => *Prop -> *Prop
- \def "logical strict existence"
+ \def "unrestricted strict logical existence"
EX = [p:*Obj->*Prop] Ex([x:*Obj] And(p(x), [y:*Obj] p(y) -> Id(x, y)))
: (*Obj -> *Prop) -> *Prop