---

Step * of Lemma pscm-presheaf-fun-family

No Annotations
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A,B:{X ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X). ∀I:cat-ob(C). ∀a:Delta(I).
  (presheaf-fun-family(C; X; A; B; I; (s)a) = presheaf-fun-family(C; Delta; (A)s; (B)s; I; a) ∈ Type)
BY
{ Auto }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {X ⊢ _}
5. B : {X ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
⊢ presheaf-fun-family(C; X; A; B; I; (s)a) = presheaf-fun-family(C; Delta; (A)s; (B)s; I; a) ∈ Type

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X,Delta:ps\_context\{j:l\}(C).  \mforall{}A,B:\{X  \mvdash{}  \_\}.  \mforall{}s:psc\_map\{j:l\}(C;  Delta;  X).
\mforall{}I:cat-ob(C).  \mforall{}a:Delta(I).
    (presheaf-fun-family(C;  X;  A;  B;  I;  (s)a)  =  presheaf-fun-family(C;  Delta;  (A)s;  (B)s;  I;  a))


By

---

Latex:
Auto

---

Home Index