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