---

Step * 1 of Lemma pscm-presheaf-fun-family


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
BY
{ (Unfold `presheaf-fun-family` 0 THEN RepeatFor 2 (EqCD) THEN Try (((Fold `member` 0 THEN Auto) ORELSE TrueCD))) }

1
.....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 ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
9. J : cat-ob(C)
⊢ (f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B(f((s)a))) = (f:(cat-arrow(C) J I) ⟶ u:(A)s(f(a)) ⟶ (B)s(f(a))) ∈ 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 ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
9. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B(f((s)a))
10. J : cat-ob(C)
⊢ (∀K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f((s)a)).
     ((w J f u f((s)a) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g(f((s)a)))))
= (∀K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:(A)s(f(a)).
     ((w J f u f(a) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ (B)s(g(f(a)))))
∈ Type

---

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  \mvdash{}  \_\}
6.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
7.  I  :  cat-ob(C)
8.  a  :  Delta(I)
\mvdash{}  presheaf-fun-family(C;  X;  A;  B;  I;  (s)a)  =  presheaf-fun-family(C;  Delta;  (A)s;  (B)s;  I;  a)


By

---

Latex:
(Unfold  `presheaf-fun-family`  0
  THEN  RepeatFor  2  (EqCD)
  THEN  Try  (((Fold  `member`  0  THEN  Auto)  ORELSE  TrueCD)))

---

Home Index