---

Step * 1 of Lemma presheaf-lambda_wf


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
⊢ (λb) ∈ I:cat-ob(C) ⟶ a:X(I) ⟶ ΠA B(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. a : X(I)
8. J : cat-ob(C)
9. K : cat-ob(C)
10. f : cat-arrow(C) J I
11. g : cat-arrow(C) K J
12. u : A(f(a))
⊢ (b J (f(a);u) (f(a);u) g) = (b K (cat-comp(C) K J I g f(a);(u f(a) g))) ∈ B(g((f(a);u)))

---

Latex:

---

Latex:

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{}  (\mlambda{}b)  \mmember{}  I:cat-ob(C)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  \mPi{}A  B(a)


By

---

Latex:
(RepUR  ``presheaf-pi  presheaf-lambda``  0  THEN  Auto  THEN  MemTypeCD\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index