---

Step * 1 1 2 of Lemma product-cat_wf

.....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))
BY
{ (Reduce 0 THEN MemCD) }

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

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

---

Latex:

---

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


By

---

Latex:
(Reduce  0  THEN  MemCD)

---

Home Index