---

Step * of Lemma pscm-presheaf-pi-family

No Annotations
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X). ∀I:cat-ob(C).
∀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)
BY
{ (Auto
   THEN (Assert ⌜s o p ∈ psc_map{j:l}(C; Delta.(A)s; X)⌝⋅ THENA Auto)
   THEN (InstLemma `psc-snd_wf` [⌜C⌝;⌜Delta⌝;⌜(A)s⌝]⋅ THENA Auto)
   THEN Unfold `presheaf-pi-family` 0
   THEN RepeatFor 4 (EqCDA)) }

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

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X,Delta:ps\_context\{j:l\}(C).  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.
\mforall{}s:psc\_map\{j:l\}(C;  Delta;  X).  \mforall{}I:cat-ob(C).  \mforall{}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))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}s  o  p  \mmember{}  psc\_map\{j:l\}(C;  Delta.(A)s;  X)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `psc-snd\_wf`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}(A)s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `presheaf-pi-family`  0
  THEN  RepeatFor  4  (EqCDA))

---

Home Index