---

Step * 1 1 of Lemma product-cat_wf

.....subterm..... T:t
2:n
1. A : SmallCategory
2. B : SmallCategory
⊢ <λ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))
                   >> ∈ arrow:(cat-ob(A) × cat-ob(B)) ⟶ (cat-ob(A) × cat-ob(B)) ⟶ Type
  × x:(cat-ob(A) × cat-ob(B)) ⟶ (arrow x x)
  × (x:(cat-ob(A) × cat-ob(B))
    ⟶ y:(cat-ob(A) × cat-ob(B))
    ⟶ z:(cat-ob(A) × cat-ob(B))
    ⟶ (arrow x y)
    ⟶ (arrow y z)
    ⟶ (arrow x z))
BY
{ MemCD }

1
.....subterm..... T:t
1:n
1. A : SmallCategory
2. B : SmallCategory
⊢ λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv)))) ∈ (cat-ob(A) × cat-ob(B))
  ⟶ (cat-ob(A) × cat-ob(B))
  ⟶ Type

2
.....subterm..... T:t
2:n
1. A : SmallCategory
2. B : SmallCategory
⊢ <λ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))
                   >
  > ∈ x:(cat-ob(A) × cat-ob(B)) ⟶ ((λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))) x \000Cx)
  × (x:(cat-ob(A) × cat-ob(B))
    ⟶ y:(cat-ob(A) × cat-ob(B))
    ⟶ z:(cat-ob(A) × cat-ob(B))
    ⟶ ((λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))) x y)
    ⟶ ((λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))) y z)
    ⟶ ((λxy,uv. (cat-arrow(A) (fst(xy)) (fst(uv)) × (cat-arrow(B) (snd(xy)) (snd(uv))))) x z))

3
.....eq aux..... 
1. A : SmallCategory
2. B : SmallCategory
3. arrow : (cat-ob(A) × cat-ob(B)) ⟶ (cat-ob(A) × cat-ob(B)) ⟶ Type
⊢ x:(cat-ob(A) × cat-ob(B)) ⟶ (arrow x x) × (x:(cat-ob(A) × cat-ob(B))
                                             ⟶ y:(cat-ob(A) × cat-ob(B))
                                             ⟶ z:(cat-ob(A) × cat-ob(B))
                                             ⟶ (arrow x y)
                                             ⟶ (arrow y z)
                                             ⟶ (arrow x z)) ∈ Type

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  A  :  SmallCategory
2.  B  :  SmallCategory
\mvdash{}  <\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))
                                      >>  \mmember{}  arrow:(cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  (cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  Type
    \mtimes{}  x:(cat-ob(A)  \mtimes{}  cat-ob(B))  {}\mrightarrow{}  (arrow  x  x)
    \mtimes{}  (x:(cat-ob(A)  \mtimes{}  cat-ob(B))
        {}\mrightarrow{}  y:(cat-ob(A)  \mtimes{}  cat-ob(B))
        {}\mrightarrow{}  z:(cat-ob(A)  \mtimes{}  cat-ob(B))
        {}\mrightarrow{}  (arrow  x  y)
        {}\mrightarrow{}  (arrow  y  z)
        {}\mrightarrow{}  (arrow  x  z))


By

---

Latex:
MemCD

---

Home Index