---

Step * 2 of Lemma presheaf-lambda_wf

.....set predicate..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
⊢ ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  (((λb) I a a f) = ((λb) J f(a)) ∈ ΠA B(f(a)))
BY
{ (RepUR ``presheaf-pi presheaf-lambda`` 0 THEN Auto THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
6. I : cat-ob(C)
7. J : cat-ob(C)
8. f : cat-arrow(C) J I
9. a : X(I)
⊢ (λK,g,u. (b K (cat-comp(C) K J I g f(a);u)))
= (λJ@0,f@0,u. (b J@0 (f@0(f(a));u)))
∈ (J@0:cat-ob(C) ⟶ f@0:(cat-arrow(C) J@0 J) ⟶ u:A(f@0(f(a))) ⟶ B((f@0(f(a));u)))

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

---

Latex:

---

Latex:
.....set  predicate..... 
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  b  :  \{X.A  \mvdash{}  \_:B\}
\mvdash{}  \mforall{}I,J:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}a:X(I).    (((\mlambda{}b)  I  a  a  f)  =  ((\mlambda{}b)  J  f(a)))


By

---

Latex:
(RepUR  ``presheaf-pi  presheaf-lambda``  0  THEN  Auto  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index