---

Step * 1 1 of Lemma presheaf-fun-as-presheaf-pi

.....subterm..... T:t
1:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
⊢ (λI,a. presheaf-fun-family(C; X; A; B; I; a))
= (λI,a. presheaf-pi-family(C; X; A; (B)p; I; a))
∈ (I:cat-ob(C) ⟶ X(I) ⟶ Type)
BY
{ Unfolds ``presheaf-fun-family presheaf-pi-family`` 0 }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
⊢ (λI,a. {w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ B(f(a))| 
          ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
            ((w J f u f(a) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g(f(a))))} )
= (λI,a. {w:J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ (B)p((f(a);u))| 
          ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
            ((w J f u (f(a);u) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ (B)p(g((f(a);u))))} )
∈ (I:cat-ob(C) ⟶ X(I) ⟶ Type)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X  \mvdash{}  \_\}
\mvdash{}  (\mlambda{}I,a.  presheaf-fun-family(C;  X;  A;  B;  I;  a))  =  (\mlambda{}I,a.  presheaf-pi-family(C;  X;  A;  (B)p;  I;  a))


By

---

Latex:
Unfolds  ``presheaf-fun-family  presheaf-pi-family``  0

---

Home Index