Step
*
of Lemma
sets-comp
∀[C:SmallCategory]. ∀[X:Top]. (cat-comp(sets(C; X)) ~ λAa,Bb,Dd,f,g. (cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
BY
{ ((Auto THEN (Assert C ∈ SmallCategory BY Trivial))
THEN DCat 1
THEN RepUR ``sets presheaf-elements mk-cat I_set`` 0
THEN (RWO "op-cat-comp" 0 THENA Auto)
THEN Auto) }
Latex:
Latex:
\mforall{}[C:SmallCategory]. \mforall{}[X:Top].
(cat-comp(sets(C; X)) \msim{} \mlambda{}Aa,Bb,Dd,f,g. (cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
By
Latex:
((Auto THEN (Assert C \mmember{} SmallCategory BY Trivial))
THEN DCat 1
THEN RepUR ``sets presheaf-elements mk-cat I\_set`` 0
THEN (RWO "op-cat-comp" 0 THENA Auto)
THEN Auto)
Home
Index