\require preamble

\* Intuitionistic Predicate Logic with Equality *\

\open elements \* [1] 2.1. 2.2. 3.1 *\

   \decl "logical false" False: *Prop

   \decl "logical conjunction" And: { [*Prop] [*Prop] } *Prop

   \decl "logical disjunction" Or: { [*Prop] [*Prop] } *Prop

\* implication and non-dependent abstraction are isomorphic *\
   \def "logical implication" 
      Imp = { [p:*Prop] [q:*Prop] } [p]^1 q : { [*Prop] [*Prop] } *Prop

\* comprehension and dependent abstraction are isomorphic *\
   \def "unrestricted logical comprehension"
      All = [q:[*Obj]^1 *Prop] [x:*Obj]^1 q(x) : [[*Obj]^1 *Prop] *Prop

   \decl "unrestricted logical existence" Ex: [[*Obj]^1 *Prop] *Prop

   \decl "syntactical identity" Id: { [*Obj] [*Obj] } *Prop

\close

\open abbreviations \* [1] 2.3. *\

   \def "logical negation" 
      Not = [p:*Prop] Imp(p, False) : [*Prop] *Prop

   \def "logical equivalence"
      Iff = { [p:*Prop] [q:*Prop] } And(Imp(p, q), Imp(q, p)) : { [*Prop] [*Prop] } *Prop

   \def "unrestricted strict logical existence"
      EX = [p:[*Obj]^1 *Prop] Ex([x:*Obj]^2 And(p(x), All([y:*Obj]^2 Imp(p(y), Id(x, y)))))
         : [[*Obj]^1 *Prop] *Prop

   \def "negated syntactical identity"
      NId = { [x:*Obj] [y:*Obj] } Not(Id(x, y)) : { [*Obj] [*Obj] } *Prop

\close