---

Step * of Lemma op-op-cat

∀[C:SmallCategory]. (op-cat(op-cat(C)) = C ∈ SmallCategory)
BY
{ (TACTIC:Auto THEN Symmetry THEN D 1 THEN At ⌜Type⌝EqTypeCD⋅ THEN Try (Trivial)) }

1
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)))

2
.....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)))  )

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  (op-cat(op-cat(C))  =  C)


By

---

Latex:
(TACTIC:Auto  THEN  Symmetry  THEN  D  1  THEN  At  \mkleeneopen{}Type\mkleeneclose{}EqTypeCD\mcdot{}  THEN  Try  (Trivial))

---

Home Index