Step * of Lemma type-cat_wf

TypeCat ∈ SmallCategory'
BY
(Unfold `type-cat` THEN At ⌜𝕌{i''}⌝MemTypeCD⋅}

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

2
.....set predicate..... 
let ob,arrow,id,comp = <Type, λI,J. (I ⟶ J), λI,x. x, λI,J,K,f,g. (g f)> 
in (∀x,y:ob. ∀f:arrow y.  (((comp (id x) f) f ∈ (arrow y)) ∧ ((comp (id y)) f ∈ (arrow y))))
   ∧ (∀x,y,z,w:ob. ∀f:arrow y. ∀g:arrow z. ∀h:arrow w.
        ((comp (comp g) h) (comp (comp h)) ∈ (arrow w)))  

3
.....wf..... 
1. cat ob:𝕌'
× arrow:ob ⟶ ob ⟶ 𝕌'
× x:ob ⟶ (arrow x)
× (x:ob ⟶ y:ob ⟶ z:ob ⟶ (arrow y) ⟶ (arrow z) ⟶ (arrow z))
⊢ let ob,arrow,id,comp cat 
  in (∀x,y:ob. ∀f:arrow y.  (((comp (id x) f) f ∈ (arrow y)) ∧ ((comp (id y)) f ∈ (arrow y))))
     ∧ (∀x,y,z,w:ob. ∀f:arrow y. ∀g:arrow z. ∀h:arrow w.
          ((comp (comp g) h) (comp (comp h)) ∈ (arrow w)))   ∈ 𝕌{i 2}


Latex:


Latex:
TypeCat  \mmember{}  SmallCategory'


By


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




Home Index