---

Step * of Lemma type-cat_wf

No Annotations
TypeCat ∈ SmallCategory'
BY
{ TACTIC:(Unfold `type-cat` 0 THEN At ⌜𝕌''⌝MemTypeCD⋅) }

1
<Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g o f)> ∈ ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× x:ob ⟶ (arrow x x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow x y) ⟶ (arrow y z) ⟶ (arrow x z))

2
.....set predicate..... 
let ob,arrow,id,comp = <Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g o f)> 
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
.....wf..... 
1. cat : ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× 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)))   ∈ 𝕌{i 2}

---

Latex:

---

Latex:
No  Annotations
TypeCat  \mmember{}  SmallCategory'


By

---

Latex:
TACTIC:(Unfold  `type-cat`  0  THEN  At  \mkleeneopen{}\mBbbU{}''\mkleeneclose{}MemTypeCD\mcdot{})

---

Home Index