---

Step * 1 of Lemma op-op-cat


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)))  
⊢ C
= op-cat(op-cat(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)))
BY
{ TACTIC:(Thin (-1) THEN RepeatFor 3 (D -1) THEN RepUR ``op-cat`` 0 THEN RepeatFor 3 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
2:n
1. ob : Type
2. arrow : ob ⟶ ob ⟶ Type
3. C3 : x:ob ⟶ (arrow x x)
4. C4 : x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z)
⊢ C4 = (λx,y,z,f,g. (C4 x y z f g)) ∈ (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))

---

Latex:

---

Latex:

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))))   
\mvdash{}  C  =  op-cat(op-cat(C))


By

---

Latex:
TACTIC:(Thin  (-1)
                THEN  RepeatFor  3  (D  -1)
                THEN  RepUR  ``op-cat``  0
                THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index