---

Step * 1 of Lemma presheaf-type-ap-morph-comp-eq


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. I : cat-ob(C)
5. J : cat-ob(C)
6. K : cat-ob(C)
7. f : cat-arrow(C) J I
8. g : cat-arrow(C) K J
9. a : X(I)
10. b : X(J)
11. u : A(a)
12. b = f(a) ∈ X(J)
⊢ ((u a f) b g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a))
BY
{ StrengthenEquation (-1) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. I : cat-ob(C)
5. J : cat-ob(C)
6. K : cat-ob(C)
7. f : cat-arrow(C) J I
8. g : cat-arrow(C) K J
9. a : X(I)
10. b : X(J)
11. u : A(a)
12. b = f(a) ∈ X(J)
13. b = f(a) ∈ {z:X(J)| (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))} 
⊢ ((u a f) b g) = (u a cat-comp(C) K J I g f) ∈ A(cat-comp(C) K J I g f(a))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  I  :  cat-ob(C)
5.  J  :  cat-ob(C)
6.  K  :  cat-ob(C)
7.  f  :  cat-arrow(C)  J  I
8.  g  :  cat-arrow(C)  K  J
9.  a  :  X(I)
10.  b  :  X(J)
11.  u  :  A(a)
12.  b  =  f(a)
\mvdash{}  ((u  a  f)  b  g)  =  (u  a  cat-comp(C)  K  J  I  g  f)


By

---

Latex:
StrengthenEquation  (-1)

---

Home Index