---

Step * 1 of Lemma presheaf-pi-family-comp


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. s : psc_map{j:l}(C; Delta; X)
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : Delta(I)
9. A : {X ⊢ _}
10. B : {X.A ⊢ _}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u))
12. ∀J,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);u) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g((f((s)a);u))))
13. J@0 : cat-ob(C)
14. K : cat-ob(C)
15. f@0 : cat-arrow(C) J@0 J
16. g : cat-arrow(C) K J@0
17. u : A(f@0((s)f(a)))
⊢ (w J@0 (cat-comp(C) J@0 J I f@0 f) u ((s)f@0(f(a));u) g)
= (w K (cat-comp(C) K J I (cat-comp(C) K J@0 J g f@0) f) (u (s)f@0(f(a)) g))
∈ B(g(((s)f@0(f(a));u)))
BY
{ (RenameVar `H' (-5)
   THEN RenameVar `h' (-3)
   THEN (InstHyp [⌜H⌝;⌜K⌝;⌜cat-comp(C) H J I h f⌝;⌜g⌝;⌜u⌝] (-6)⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN 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. s : psc_map{j:l}(C; Delta; X)
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : Delta(I)
9. A : {X ⊢ _}
10. B : {X.A ⊢ _}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u))
12. ∀J,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);u) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g((f((s)a);u))))
13. H : cat-ob(C)
14. K : cat-ob(C)
15. h : cat-arrow(C) H J
16. g : cat-arrow(C) K H
17. u : A(h((s)f(a)))
18. (w H (cat-comp(C) H J I h f) u (cat-comp(C) H J I h f((s)a);u) g)
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B(g((cat-comp(C) H J I h f((s)a);u)))
⊢ B(g(((s)h(f(a));u))) = B(g((cat-comp(C) H J I h f((s)a);u))) ∈ 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. s : psc_map{j:l}(C; Delta; X)
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : Delta(I)
9. A : {X ⊢ _}
10. B : {X.A ⊢ _}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u))
12. ∀J,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);u) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g((f((s)a);u))))
13. H : cat-ob(C)
14. K : cat-ob(C)
15. h : cat-arrow(C) H J
16. g : cat-arrow(C) K H
17. u : A(h((s)f(a)))
18. (w H (cat-comp(C) H J I h f) u (cat-comp(C) H J I h f((s)a);u) g)
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B(g((cat-comp(C) H J I h f((s)a);u)))
⊢ (w H (cat-comp(C) H J I h f) u ((s)h(f(a));u) g)
= (w H (cat-comp(C) H J I h f) u (cat-comp(C) H J I h f((s)a);u) g)
∈ B(g(((s)h(f(a));u)))

3
.....subterm..... T:t
3:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. s : psc_map{j:l}(C; Delta; X)
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : Delta(I)
9. A : {X ⊢ _}
10. B : {X.A ⊢ _}
11. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u))
12. ∀J,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);u) g) = (w K (cat-comp(C) K J I g f) (u f((s)a) g)) ∈ B(g((f((s)a);u))))
13. H : cat-ob(C)
14. K : cat-ob(C)
15. h : cat-arrow(C) H J
16. g : cat-arrow(C) K H
17. u : A(h((s)f(a)))
18. (w H (cat-comp(C) H J I h f) u (cat-comp(C) H J I h f((s)a);u) g)
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B(g((cat-comp(C) H J I h f((s)a);u)))
⊢ (w K (cat-comp(C) K J I (cat-comp(C) K H J g h) f) (u (s)h(f(a)) g))
= (w K (cat-comp(C) K H I g (cat-comp(C) H J I h f)) (u cat-comp(C) H J I h f((s)a) g))
∈ B(g(((s)h(f(a));u)))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  s  :  psc\_map\{j:l\}(C;  Delta;  X)
5.  I  :  cat-ob(C)
6.  J  :  cat-ob(C)
7.  f  :  cat-arrow(C)  J  I
8.  a  :  Delta(I)
9.  A  :  \{X  \mvdash{}  \_\}
10.  B  :  \{X.A  \mvdash{}  \_\}
11.  w  :  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A(f((s)a))  {}\mrightarrow{}  B((f((s)a);u))
12.  \mforall{}J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}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)))
13.  J@0  :  cat-ob(C)
14.  K  :  cat-ob(C)
15.  f@0  :  cat-arrow(C)  J@0  J
16.  g  :  cat-arrow(C)  K  J@0
17.  u  :  A(f@0((s)f(a)))
\mvdash{}  (w  J@0  (cat-comp(C)  J@0  J  I  f@0  f)  u  ((s)f@0(f(a));u)  g)
=  (w  K  (cat-comp(C)  K  J  I  (cat-comp(C)  K  J@0  J  g  f@0)  f)  (u  (s)f@0(f(a))  g))


By

---

Latex:
(RenameVar  `H'  (-5)
  THEN  RenameVar  `h'  (-3)
  THEN  (InstHyp  [\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}cat-comp(C)  H  J  I  h  f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  EqCDA)

---

Home Index