---

Step * 3 of Lemma poset-cat_wf

.....wf..... 
1. J : Cname List
2. cat : ob:Type
× arrow:ob ⟶ ob ⟶ Type
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))
⊢ let ob,arrow,id,comp = cat 
  in (∀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))))
     ∧ (∀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)))   ∈ Type
BY
{ ((RepeatFor 3 (D -1) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  J  :  Cname  List
2.  cat  :  ob:Type
\mtimes{}  arrow:ob  {}\mrightarrow{}  ob  {}\mrightarrow{}  Type
\mtimes{}  x:ob  {}\mrightarrow{}  (arrow  x  x)
\mtimes{}  (x:ob  {}\mrightarrow{}  y:ob  {}\mrightarrow{}  z:ob  {}\mrightarrow{}  (arrow  x  y)  {}\mrightarrow{}  (arrow  y  z)  {}\mrightarrow{}  (arrow  x  z))
\mvdash{}  let  ob,arrow,id,comp  =  cat 
    in  (\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)))
          \mwedge{}  (\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))))      \mmember{}  Type


By

---

Latex:
((RepeatFor  3  (D  -1)  THEN  Reduce  0)  THEN  Auto)

---

Home Index