---

Step * 1 of Lemma pscm-presheaf-pi


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)
⊢ (ΠA B)s
= Delta ⊢ Π(A)s (B)(s o p;q)
∈ (A:I:cat-ob(C) ⟶ Delta(I) ⟶ Type × (I:cat-ob(C)
                                       ⟶ J:cat-ob(C)
                                       ⟶ f:(cat-arrow(C) J I)
                                       ⟶ a:Delta(I)
                                       ⟶ (A I a)
                                       ⟶ (A J f(a))))
BY
{ (RepUR ``presheaf-pi pscm-ap-type`` 0 THEN Fold `pscm-ap-type` 0 THEN EqCD) }

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)
⊢ (λ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)

2
.....subterm..... T:t
2: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,J,f,a,u,K,g. (u K (cat-comp(C) K J I g f)))
= (λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f)))
∈ (I:cat-ob(C)
  ⟶ J:cat-ob(C)
  ⟶ f:(cat-arrow(C) J I)
  ⟶ a:Delta(I)
  ⟶ ((λI,a. presheaf-pi-family(C; X; A; B; I; (s)a)) I a)
  ⟶ ((λI,a. presheaf-pi-family(C; X; A; B; I; (s)a)) J f(a)))

3
.....eq aux..... 
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. A1 : I:cat-ob(C) ⟶ Delta(I) ⟶ Type
⊢ istype(I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:Delta(I) ⟶ (A1 I a) ⟶ (A1 J f(a)))

---

Latex:

---

Latex:

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{}  (\mPi{}A  B)s  =  Delta  \mvdash{}  \mPi{}(A)s  (B)(s  o  p;q)


By

---

Latex:
(RepUR  ``presheaf-pi  pscm-ap-type``  0  THEN  Fold  `pscm-ap-type`  0  THEN  EqCD)

---

Home Index