---

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

.....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
BY
{ RepeatFor 2 (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 ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
9. J : cat-ob(C)
⊢ (cat-arrow(C) J) = (cat-arrow(C) J) ∈ (y:cat-ob(C) ⟶ 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. J : cat-ob(C)
⊢ I = I ∈ cat-ob(C)

3
.....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 ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. I : cat-ob(C)
8. a : Delta(I)
9. J : cat-ob(C)
10. f : cat-arrow(C) J I
⊢ A(f((s)a)) = (A)s(f(a)) ∈ Type

4
.....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)
10. f : cat-arrow(C) J I
11. u : A(f((s)a))
⊢ B(f((s)a)) = (B)s(f(a)) ∈ Type

---

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  \mvdash{}  \_\}
6.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
7.  I  :  cat-ob(C)
8.  a  :  Delta(I)
9.  J  :  cat-ob(C)
\mvdash{}  (f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A(f((s)a))  {}\mrightarrow{}  B(f((s)a)))
=  (f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:(A)s(f(a))  {}\mrightarrow{}  (B)s(f(a)))


By

---

Latex:
RepeatFor  2  (EqCD)

---

Home Index