(def-quasi-constructor m-composition 
    "lambda(f:[ind_2,ind_3],g:[ind_1,ind_2], lambda(x:ind_1, f(g(x))))"
    (language pure-generic-theory-3)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-domain 
    "lambda(f:[ind_1,ind_2], indic(x:ind_1, #(f(x))))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-range 
    "lambda(f:[ind_1,ind_2], indic(y:ind_2, forsome(x:ind_1, y=f(x))))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-image 
    "lambda(f:[ind_1,ind_2],a:sets[ind_1],
          indic(y:ind_2, forsome(x:ind_1, (x in a) and y=f(x))))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-inverse-image 
    "lambda(f:[ind_1,ind_2],b:sets[ind_2], b oo f)"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-inverse 
    "lambda(f:[ind_1,ind_2], 
          lambda(x:ind_2, iota(y:ind_1, f(y)=x)))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-id 
    "lambda(a:sets[ind_1],
          lambda(x:ind_1, if(x in a, x, ?ind_1)))"
    (language pure-generic-theory-1)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-restrict 
    "lambda(f:[ind_1,ind_2],a:sets[ind_1],
          lambda(x:ind_1, if(x in a, f(x), ?ind_2)))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-restrict2 
    "lambda(f:[ind_1,ind_2,ind_3],a:sets[ind_1],b:sets[ind_2],
          lambda(x:ind_1,y:ind_2, if(x in a and y in b, f(x,y), ?ind_3)))"
    (language pure-generic-theory-3)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-surjective? 
    "lambda(f:[ind_1,ind_2], 
          forall(x:ind_1, x in dom(f)) and forall(y:ind_2, y in ran(f)))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-injective? 
    "lambda(f:[ind_1,ind_2], 
          forall(x_1,x_2:ind_1, f(x_1)=f(x_2) implies x_1=x_2))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-bijective? 
    "lambda(f:[ind_1,ind_2], surjective_q(f) and injective_q(f))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-surjective-on? 
    "lambda(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2], 
          dom(f)=a and ran(f)=b)"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-injective-on? 
    "lambda(f:[ind_1,ind_2],a:sets[ind_1],
          forall(x_1,x_2:ind_1, 
              ((x_1 in a) and (x_2 in a) and f(x_1)=f(x_2)) implies x_1=x_2))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))

(def-quasi-constructor m-bijective-on? 
    "lambda(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
          surjective_on_q(f,a,b) and injective_on_q(f,a))"
    (language pure-generic-theory-2)
    (fixed-theories the-kernel-theory))