---

Step * 1 1 of Lemma unit-set-presheaf-type


1. C : SmallCategory
2. I : cat-ob(C)
3. A : Base
4. I@0 : Base
5. J : Base
6. f : Base
7. a : Base
8. @0 : Base
⊢ f(a) ~ cat-comp(C) J I@0 I f a
BY
{ Computation }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  I  :  cat-ob(C)
3.  A  :  Base
4.  I@0  :  Base
5.  J  :  Base
6.  f  :  Base
7.  a  :  Base
8.  @0  :  Base
\mvdash{}  f(a)  \msim{}  cat-comp(C)  J  I@0  I  f  a


By

---

Latex:
Computation

---

Home Index