---

Step * of Lemma mk-cat_wf

∀[ob:Type]. ∀[arrow:ob ⟶ ob ⟶ Type]. ∀[id:x:ob ⟶ arrow[x;x]]. ∀[comp:x:ob
                                                                        ⟶ y:ob
                                                                        ⟶ z:ob
                                                                        ⟶ arrow[x;y]
                                                                        ⟶ arrow[y;z]
                                                                        ⟶ arrow[x;z]].
  (Cat(ob = ob;
       arrow(x,y) = arrow[x;y];
       id(a) = id[a];
       comp(u,v,w,f,g) = comp[u;v;w;f;g]) ∈ SmallCategory) supposing 
     ((∀x,y,z,w:ob. ∀f:arrow[x;y]. ∀g:arrow[y;z]. ∀h:arrow[z;w].
         (comp[x;z;w;comp[x;y;z;f;g];h] = comp[x;y;w;f;comp[y;z;w;g;h]] ∈ arrow[x;w])) and 
     (∀x,y:ob. ∀f:arrow[x;y].  ((comp[x;x;y;id[x];f] = f ∈ arrow[x;y]) ∧ (comp[x;y;y;f;id[y]] = f ∈ arrow[x;y]))))
BY
{ (Auto
   THEN (At ⌜Type⌝ MemTypeCD⋅ THENW Auto)
   THEN RepUR ``mk-cat`` 0
   THEN Try ((D 0 THEN Trivial))
   THEN RepUR  ``so_apply`` 0⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[ob:Type].  \mforall{}[arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type].  \mforall{}[id:x:ob  {}\mrightarrow{}  arrow[x;x]].  \mforall{}[comp:x:ob
                                                                                                                                                {}\mrightarrow{}  y:ob
                                                                                                                                                {}\mrightarrow{}  z:ob
                                                                                                                                                {}\mrightarrow{}  arrow[x;y]
                                                                                                                                                {}\mrightarrow{}  arrow[y;z]
                                                                                                                                                {}\mrightarrow{}  arrow[x;z]].
    (Cat(ob  =  ob;
              arrow(x,y)  =  arrow[x;y];
              id(a)  =  id[a];
              comp(u,v,w,f,g)  =  comp[u;v;w;f;g])  \mmember{}  SmallCategory)  supposing 
          ((\mforall{}x,y,z,w:ob.  \mforall{}f:arrow[x;y].  \mforall{}g:arrow[y;z].  \mforall{}h:arrow[z;w].
                  (comp[x;z;w;comp[x;y;z;f;g];h]  =  comp[x;y;w;f;comp[y;z;w;g;h]]))  and 
          (\mforall{}x,y:ob.  \mforall{}f:arrow[x;y].    ((comp[x;x;y;id[x];f]  =  f)  \mwedge{}  (comp[x;y;y;f;id[y]]  =  f))))


By

---

Latex:
(Auto
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THENW  Auto)
  THEN  RepUR  ``mk-cat``  0
  THEN  Try  ((D  0  THEN  Trivial))
  THEN  RepUR    ``so\_apply``  0\mcdot{}
  THEN  Auto)

---

Home Index