---

Step * 1 of Lemma presheaf-type-rev-iso_wf


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : I:cat-ob(C) ⟶ X(I) ⟶ Type
4. x1 : I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a))
5. ∀I:cat-ob(C). ∀a:X(I). ∀u:A I a.  ((x1 I I (cat-id(C) I) a u) = u ∈ (A I a))
6. ∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I). ∀u:A I a.
     ((x1 I K (cat-comp(C) K J I g f) a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A K cat-comp(C) K J I g f(a)))
7. I2 : cat-ob(C)
8. p1 : X(I2)
9. I1 : cat-ob(C)
10. q1 : X(I1)
11. I : cat-ob(C)
12. z1 : X(I)
13. f : cat-arrow(C) I1 I2
14. f(p1) = q1 ∈ (X I1)
15. g : cat-arrow(C) I I1
16. g(q1) = z1 ∈ (X I)
17. x : A I2 p1
⊢ (x1 I2 I (cat-comp(C) I I1 I2 g f) p1 x) = (x1 I1 I g q1 (x1 I2 I1 f p1 x)) ∈ (A I z1)
BY
{ SwapVars `I' `I2' }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : I:cat-ob(C) ⟶ X(I) ⟶ Type
4. x1 : I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a))
5. ∀I:cat-ob(C). ∀a:X(I). ∀u:A I a.  ((x1 I I (cat-id(C) I) a u) = u ∈ (A I a))
6. ∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I). ∀u:A I a.
     ((x1 I K (cat-comp(C) K J I g f) a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A K cat-comp(C) K J I g f(a)))
7. I : cat-ob(C)
8. p1 : X(I)
9. I1 : cat-ob(C)
10. q1 : X(I1)
11. I2 : cat-ob(C)
12. z1 : X(I2)
13. f : cat-arrow(C) I1 I
14. f(p1) = q1 ∈ (X I1)
15. g : cat-arrow(C) I2 I1
16. g(q1) = z1 ∈ (X I2)
17. x : A I p1
⊢ (x1 I I2 (cat-comp(C) I2 I1 I g f) p1 x) = (x1 I1 I2 g q1 (x1 I I1 f p1 x)) ∈ (A I2 z1)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  Type
4.  x1  :  I:cat-ob(C)  {}\mrightarrow{}  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  (A  I  a)  {}\mrightarrow{}  (A  J  f(a))
5.  \mforall{}I:cat-ob(C).  \mforall{}a:X(I).  \mforall{}u:A  I  a.    ((x1  I  I  (cat-id(C)  I)  a  u)  =  u)
6.  \mforall{}I,J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}a:X(I).  \mforall{}u:A  I  a.
          ((x1  I  K  (cat-comp(C)  K  J  I  g  f)  a  u)  =  (x1  J  K  g  f(a)  (x1  I  J  f  a  u)))
7.  I2  :  cat-ob(C)
8.  p1  :  X(I2)
9.  I1  :  cat-ob(C)
10.  q1  :  X(I1)
11.  I  :  cat-ob(C)
12.  z1  :  X(I)
13.  f  :  cat-arrow(C)  I1  I2
14.  f(p1)  =  q1
15.  g  :  cat-arrow(C)  I  I1
16.  g(q1)  =  z1
17.  x  :  A  I2  p1
\mvdash{}  (x1  I2  I  (cat-comp(C)  I  I1  I2  g  f)  p1  x)  =  (x1  I1  I  g  q1  (x1  I2  I1  f  p1  x))


By

---

Latex:
SwapVars  `I'  `I2'

---

Home Index