---

Step * 1 3 1 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
⊢ ∀f:{f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
    (((cat-comp(op-cat(C)) A2 A A f (cat-id(op-cat(C)) A))
    = f
    ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} )
    ∧ ((cat-comp(op-cat(C)) A2 A2 A (cat-id(op-cat(C)) A2) f)
      = f
      ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} ))
BY
{ At ⌜Type⌝ (D 0)⋅ }

1
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
7. f : {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
⊢ ((cat-comp(op-cat(C)) A2 A A f (cat-id(op-cat(C)) A)) = f ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} \000C)
∧ ((cat-comp(op-cat(C)) A2 A2 A (cat-id(op-cat(C)) A2) f)
  = f
  ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} )

2
.....wf..... 
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
⊢ istype({f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} )

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  A  :  cat-ob(op-cat(C))
4.  A1  :  P  A
5.  A2  :  cat-ob(op-cat(C))
6.  B1  :  P  A2
\mvdash{}  \mforall{}f:\{f:cat-arrow(op-cat(C))  A2  A|  (P  A2  A  f  B1)  =  A1\} 
        (((cat-comp(op-cat(C))  A2  A  A  f  (cat-id(op-cat(C))  A))  =  f)
        \mwedge{}  ((cat-comp(op-cat(C))  A2  A2  A  (cat-id(op-cat(C))  A2)  f)  =  f))


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index