---

Step * 1 2 of Lemma pscm-presheaf-pi

.....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)))
BY
{ (RepeatFor 5 ((EqCD THENA Auto)) THEN Reduce (-1) THEN Reduce 0 THEN Fold `member` 0) }

1
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. J : cat-ob(C)
9. f : cat-arrow(C) J I
10. a : Delta(I)
11. u : presheaf-pi-family(C; X; A; B; I; (s)a)
⊢ λK,g. (u K (cat-comp(C) K J I g f)) ∈ presheaf-pi-family(C; X; A; B; J; (s)f(a))

---

Latex:

---

Latex:
.....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  \mvdash{}  \_\}
5.  B  :  \{X.A  \mvdash{}  \_\}
6.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
\mvdash{}  (\mlambda{}I,J,f,a,u,K,g.  (u  K  (cat-comp(C)  K  J  I  g  f)))  =  (\mlambda{}I,J,f,a,w,K,g.  (w  K  (cat-comp(C)  K  J  I  g  f)))


By

---

Latex:
(RepeatFor  5  ((EqCD  THENA  Auto))  THEN  Reduce  (-1)  THEN  Reduce  0  THEN  Fold  `member`  0)

---

Home Index