---

Step * 1 1 of Lemma pscm-presheaf-pi

.....subterm..... T:t
1:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {X ⊢ _}
5. B : {X.A ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
⊢ (λI,a. presheaf-pi-family(C; X; A; B; I; (s)a))
= (λI,a. presheaf-pi-family(C; Delta; (A)s; (B)(s o p;q); I; a))
∈ (I:cat-ob(C) ⟶ Delta(I) ⟶ Type)
BY
{ RepeatFor 2 ((EqCD THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
RepeatFor  2  ((EqCD  THENA  Auto))

---

Home Index