---

Step * 1 of Lemma presheaf-fun_wf


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
⊢ <λI,a. presheaf-fun-family(C; X; A; B; I; a), λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f))> ∈ A:I:cat-ob(C) ⟶ X(I) ─\000C→ Type
  × (I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a)))
BY
{ (MemCD THEN Reduce 0 THEN Auto THEN D -1 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
5. I : cat-ob(C)
6. J : cat-ob(C)
7. f : cat-arrow(C) J I
8. a : X(I)
9. w : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f(a)) ⟶ B(f(a))
10. ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A(f(a)).
      ((w J f u f(a) g) = (w K (cat-comp(C) K J I g f) (u f(a) g)) ∈ B(g(f(a))))
11. J@0 : cat-ob(C)
12. K : cat-ob(C)
13. f@0 : cat-arrow(C) J@0 J
14. g : cat-arrow(C) K J@0
15. u : A(f@0(f(a)))
⊢ (w J@0 (cat-comp(C) J@0 J I f@0 f) u f@0(f(a)) g)
= (w K (cat-comp(C) K J I (cat-comp(C) K J@0 J g f@0) f) (u f@0(f(a)) g))
∈ B(g(f@0(f(a))))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X  \mvdash{}  \_\}
\mvdash{}  <\mlambda{}I,a.  presheaf-fun-family(C;  X;  A;  B;  I;  a),  \mlambda{}I,J,f,a,w,K,g.  (w  K  (cat-comp(C)  K  J  I  g  f))>  \mmember{}  A:I\000C:cat-ob(C)
    {}\mrightarrow{}  X(I)
    {}\mrightarrow{}  Type  \mtimes{}  (I:cat-ob(C)  {}\mrightarrow{}  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  (A  I  a)  {}\mrightarrow{}  (A  J  f(a)))


By

---

Latex:
(MemCD  THEN  Reduce  0  THEN  Auto  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index