---

Step * of Lemma presheaf-type-ap-morph-id

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[I:cat-ob(C)]. ∀[f:cat-arrow(C) I I]. ∀[a:X(I)]. ∀[u:A(a)].
  (u a f) = u ∈ A(a) supposing f = (cat-id(C) I) ∈ (cat-arrow(C) I I)
BY
{ (Auto THEN (StrongHypSubst  (-1) 0 THENA Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. I : cat-ob(C)
5. f : cat-arrow(C) I I
6. a : X(I)
7. u : A(a)
8. f = (cat-id(C) I) ∈ (cat-arrow(C) I I)
⊢ (u a cat-id(C) I) = u ∈ A(a)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[I:cat-ob(C)].  \mforall{}[f:cat-arrow(C)  I  I].
\mforall{}[a:X(I)].  \mforall{}[u:A(a)].
    (u  a  f)  =  u  supposing  f  =  (cat-id(C)  I)


By

---

Latex:
(Auto  THEN  (StrongHypSubst    (-1)  0  THENA  Auto))

---

Home Index