<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
#!/usr/local/bin/aut

{ ----------------------------- many-sorted first order logic -----------15-- }

* prop : TYPE := PRIM
* [a:prop] proof : TYPE := PRIM
* sort : TYPE := PRIM
* [s:sort] elt : TYPE := PRIM

* false : prop := PRIM
a * [b:prop] imp : prop := PRIM
s * [p:[z,elt(s)]prop] for : prop := PRIM
s * [x:elt(s)][y:elt(s)] eq : prop := PRIM

a * not : prop := imp(a,false)
b * and : prop := not(imp(a,not(b)))
b * iff : prop := and(imp(a,b),imp(b,a))
p * ex : prop := not(for([z,elt(s)]not(<z>p)))
p * unique : prop :=
  for([z,elt(s)]imp(<z>p,for([z',elt(s)]imp(<z'>p,eq(z,z')))))
p * ex_unique : prop := and(ex,unique)

b * [_1:[_,proof(a)]proof(b)] imp_intro : proof(imp(a,b)) := PRIM
b * [_1:proof(imp(a,b))][_2:proof(a)] imp_elim : proof(b) := PRIM
p * [_1:[z,elt(s)]proof(<z>p)] for_intro : proof(for(p)) := PRIM
p * [_1:proof(for(p))][z:elt(s)] for_elim : proof(<z>p) := PRIM
a * [_1:proof(not(not(a)))] classical : proof(a) := PRIM
x * eq_intro : proof(eq(x,x)) := PRIM
y * [_1:proof(eq(x,y))][q:[z,elt(s)]prop][_2:proof(<x>q)]
    eq_elim : proof(<y>q) := PRIM

{ ----------------------------- category theory --------------------------8-- }

* object_sort : sort := PRIM
* arrow_sort : sort := PRIM

* object : TYPE := elt(object_sort)
* arrow : TYPE := elt(arrow_sort)

* [p:[A:object]prop]
  for_object : prop := for(object_sort,p)
  ex_object : prop := ex(object_sort,p)
* [p:[A:arrow]prop]
  for_arrow : prop := for(arrow_sort,p)
  ex_arrow : prop := ex(arrow_sort,p)
  ex_unique_arrow : prop := ex_unique(arrow_sort,p)
* [f:arrow][g:arrow] eq_arrow : prop := eq(arrow_sort,f,g)

* [A:object] Id : arrow := PRIM
* [f:arrow][A:object][B:object] maps : prop := PRIM
f * [g:arrow][h:arrow] comp : prop := PRIM

* [f:arrow][A:object][B:object] axiom_1 :
  proof(imp(maps(f,A,B),and(comp(f,Id(A),f),comp(Id(B),f,f))))
    := PRIM
f * [g:arrow] axiom_2 :
  proof(iff(ex_object([A,object]ex_object([B,object]ex_object([C,object]
      and(maps(f,A,B),maps(g,B,C))))),
    ex_arrow([h,arrow]comp(g,f,h)))) := PRIM
g * [h:arrow][k:arrow][i:arrow][j:arrow] axiom_3 :
  proof(imp(and(comp(g,f,k),and(comp(h,k,j),comp(h,g,i))),
    comp(i,f,j))) := PRIM

{ ----------------------------- terminal object and cartesian products ---9-- }

* 1 : object := PRIM
* [A:object][B:object] prod_object : object := PRIM
g * prod_arrow : arrow := PRIM
B * p1 : arrow := PRIM
  p2 : arrow := PRIM

A * axiom_4 : proof(ex_unique_arrow([f,arrow]maps(f,A,1))) := PRIM
B * axiom_5 :
  proof(and(maps(p1(A,B),prod_object(A,B),A),maps(p2(A,B),prod_object(A,B),B)))
    := PRIM
g * [A:object][B:object][T:object] axiom_6 :
  proof(imp(and(maps(f,T,A),maps(g,T,B)),
    ex_unique_arrow([u,arrow]and(maps(u,T,prod_object(A,B)),
      and(comp(p1(A,B),u,f),comp(p2(A,B),u,g)))))) := PRIM
B * [C:object][D:object] axiom_7 :
  proof(imp(and(maps(f,A,B),maps(g,C,D)),
    and(maps(prod_arrow(f,g),prod_object(A,C),prod_object(B,D)),
      for_arrow([h,arrow]for_arrow([k,arrow]
        imp(and(comp(f,p1(A,C),h),comp(g,p2(A,C),k)),
          and(comp(p1(B,D),prod_arrow(f,g),h),
            comp(p2(B,D),prod_arrow(f,g),k)))))))) := PRIM

{ ----------------------------- non-trivial Boolean topos ---------------10-- }

* 2 : object := PRIM
* i1 : arrow := PRIM
  i2 : arrow := PRIM
* [A:object][B:object] funcs : object := PRIM
B * eval : arrow := PRIM
f * monic : prop := PRIM

# axiom_8
f * [A:object][B:object][T:object] axiom_9 :
  proof(imp(maps(f,prod_object(T,A),B),
    ex_unique_arrow([u,arrow]and(maps(u,T,funcs(A,B)),
      comp(eval(A,B),prod_arrow(u,Id(A)),f))))) := PRIM
g * [A:object] axiom_10 :
  proof(and(not(eq_arrow(i1,i2)),imp(and(maps(f,1,A),maps(g,1,A)),
      ex_unique_arrow([u,arrow]and(maps(u,1,A),
        and(comp(u,i1,g),comp(u,i2,g))))))) := PRIM
f * axiom_11 :
  proof(iff(monic(f),for_arrow([g,arrow]for_arrow([h,arrow]for_arrow([k,arrow]
    imp(and(comp(f,g,k),comp(f,h,k)),eq_arrow(g,h))))))) := PRIM
f * [A:object][B:object][u:arrow][h:arrow][k:arrow][j:arrow] axiom_12 :
  proof(and(imp(and(monic(f),maps(f,A,B)),
      ex_unique_arrow([u,arrow]and(maps(u,B,2),
        for_arrow([h,arrow]for_arrow([k,arrow]for_arrow([j,arrow]
          imp(and(comp(i1,k,j),comp(u,h,j)),
            ex_unique_arrow([v,arrow]comp(f,v,h))))))))),
    imp(and(maps(u,B,2),and(comp(i1,k,j),comp(u,h,j))),
      ex_unique_arrow([v,arrow]comp(f,v,h))))) := PRIM

{ ----------------------------- natural numbers --------------------------1-- }

* axiom_13 :
  proof(ex_object([N,object]ex_arrow([0,arrow]ex_arrow([s,arrow]
    and(and(maps(0,1,N),maps(s,N,N)),
      for_object([A,object]for_arrow([x,arrow]for_arrow([f,arrow]
        imp(and(maps(x,1,A),maps(f,A,A)),
          ex_unique_arrow([u,arrow]and(maps(u,N,A),
            ex_arrow([h,arrow]ex_arrow([k,arrow]
              and(comp(u,0,x),and(comp(u,s,k),comp(f,u,k))))))))))))))))
    := PRIM

{ ----------------------------- well-pointed topos with choice -----------2-- }

g * [A:object][B:object] axiom_14 :
  proof(imp(and(and(maps(f,A,B),maps(g,A,B)),
      for_arrow([k,arrow]for_arrow([h,arrow]imp(maps(h,1,A),
        iff(comp(f,h,k),comp(g,h,k)))))),
    eq_arrow(f,g))) := PRIM
f * [A:object][B:object] axiom_15 :
  proof(imp(and(maps(f,A,B),
      for_arrow([h,arrow]imp(maps(h,1,B),
        ex_arrow([k,arrow]and(maps(k,1,A),comp(f,k,h)))))),
    ex_arrow([g,arrow]and(maps(g,B,A),comp(f,g,Id(B)))))) := PRIM