---

Step * of Lemma poset-cat_wf

∀[J:Cname List]. (poset-cat(J) ∈ SmallCategory)
BY
{ (ProveWfLemma THEN At ⌜Type⌝ MemTypeCD⋅) }

1
1. J : Cname List
⊢ <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax> ∈ 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
.....set predicate..... 
1. J : Cname List
⊢ let ob,arrow,id,comp = <name-morph(J;[]), λf,g. ∀x:nameset(J). (↑f x ≤z g x), λf,x. Ax, λf,g,h,p,q,x. Ax> 
  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. 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

---

Latex:

---

Latex:
\mforall{}[J:Cname  List].  (poset-cat(J)  \mmember{}  SmallCategory)


By

---

Latex:
(ProveWfLemma  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{})

---

Home Index