Nuprl Definition : product-cat
A × B ==
<cat-ob(A) × cat-ob(B)
, λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))
, λxy.<cat-id(A) (fst(xy)), cat-id(B) (snd(xy))>
, λxy,uv,wz,F,G. <cat-comp(A) (fst(xy)) (fst(uv)) (fst(wz)) (fst(F)) (fst(G))
, cat-comp(B) (snd(xy)) (snd(uv)) (snd(wz)) (snd(F)) (snd(G))
>>
Definitions occuring in Statement :
cat-comp: cat-comp(C),
cat-id: cat-id(C),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
pi1: fst(t),
pi2: snd(t),
apply: f a,
lambda: λx.A[x],
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
cat-ob: cat-ob(C),
product: x:A × B[x],
cat-arrow: cat-arrow(C),
cat-id: cat-id(C),
lambda: λx.A[x],
pair: <a, b>,
pi1: fst(t),
apply: f a,
cat-comp: cat-comp(C),
pi2: snd(t)
FDL editor aliases :
product-cat
Latex:
A \mtimes{} B ==
<cat-ob(A) \mtimes{} cat-ob(B)
, \mlambda{}xy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) \mtimes{} (cat-arrow(B) (snd(xy)) (snd(uv))))
, \mlambda{}xy.<cat-id(A) (fst(xy)), cat-id(B) (snd(xy))>
, \mlambda{}xy,uv,wz,F,G. <cat-comp(A) (fst(xy)) (fst(uv)) (fst(wz)) (fst(F)) (fst(G))
, cat-comp(B) (snd(xy)) (snd(uv)) (snd(wz)) (snd(F)) (snd(G))
>>
Date html generated:
2020_05_20-AM-07_53_59
Last ObjectModification:
2017_01_09-AM-11_11_36
Theory : small!categories
Home
Index