---

Step * 2 1 1 1 of Lemma presheaf-element-map_wf


1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A@0:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (A A@0) (B A@0))
5. ∀A@0,B@0:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A@0 B@0.
     (((B A@0 B@0 g) o (m A@0)) = ((m B@0) o (A A@0 B@0 g)) ∈ ((A A@0) ⟶ (B B@0)))
6. A@0 : cat-ob(op-cat(C))
7. x1 : A A@0
8. A1 : cat-ob(op-cat(C))
9. y1 : A A1
10. x : cat-arrow(op-cat(C)) A1 A@0
11. (A A1 A@0 x y1) = x1 ∈ (A A@0)
⊢ (B A1 A@0 x (m A1 y1)) = (m A@0 x1) ∈ (B A@0)
BY
{ (InstHyp [⌜A1⌝;⌜A@0⌝;⌜x⌝] 5⋅ THENA Auto) }

1
1. C : SmallCategory
2. A : Presheaf(C)
3. B : Presheaf(C)
4. m : A@0:cat-ob(op-cat(C)) ⟶ (cat-arrow(TypeCat) (A A@0) (B A@0))
5. ∀A@0,B@0:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A@0 B@0.
     (((B A@0 B@0 g) o (m A@0)) = ((m B@0) o (A A@0 B@0 g)) ∈ ((A A@0) ⟶ (B B@0)))
6. A@0 : cat-ob(op-cat(C))
7. x1 : A A@0
8. A1 : cat-ob(op-cat(C))
9. y1 : A A1
10. x : cat-arrow(op-cat(C)) A1 A@0
11. (A A1 A@0 x y1) = x1 ∈ (A A@0)
12. ((B A1 A@0 x) o (m A1)) = ((m A@0) o (A A1 A@0 x)) ∈ ((A A1) ⟶ (B A@0))
⊢ (B A1 A@0 x (m A1 y1)) = (m A@0 x1) ∈ (B A@0)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  A  :  Presheaf(C)
3.  B  :  Presheaf(C)
4.  m  :  A@0:cat-ob(op-cat(C))  {}\mrightarrow{}  (cat-arrow(TypeCat)  (A  A@0)  (B  A@0))
5.  \mforall{}A@0,B@0:cat-ob(op-cat(C)).  \mforall{}g:cat-arrow(op-cat(C))  A@0  B@0.
          (((B  A@0  B@0  g)  o  (m  A@0))  =  ((m  B@0)  o  (A  A@0  B@0  g)))
6.  A@0  :  cat-ob(op-cat(C))
7.  x1  :  A  A@0
8.  A1  :  cat-ob(op-cat(C))
9.  y1  :  A  A1
10.  x  :  cat-arrow(op-cat(C))  A1  A@0
11.  (A  A1  A@0  x  y1)  =  x1
\mvdash{}  (B  A1  A@0  x  (m  A1  y1))  =  (m  A@0  x1)


By

---

Latex:
(InstHyp  [\mkleeneopen{}A1\mkleeneclose{};\mkleeneopen{}A@0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THENA  Auto)

---

Home Index