---

Step * 2 of Lemma op-op-cat

.....wf..... 
1. C : 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))
2. let ob,arrow,id,comp = C 
   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)))  
3. 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))
⊢ istype(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)))  )
BY
{ ((RepeatFor 3 (D -1) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  C  :  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))
2.  let  ob,arrow,id,comp  =  C 
      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))))   
3.  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{}  istype(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))))    )


By

---

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

---

Home Index