---

Step * 1 1 of Lemma psdcff-inj-injection

.....subterm..... T:t
1:n
1. C : SmallCategory
2. A : Type
3. B : Type
4. X : ps_context{j:l}(C)
5. I : cat-ob(C)
6. a : X(I)
7. a1 : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A ⟶ B
8. ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A.  ((a1 J f u) = (a1 K (cat-comp(C) K J I g f) u) ∈ B)
9. a2 : J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A ⟶ B
10. ∀J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀u:A.  ((a2 J f u) = (a2 K (cat-comp(C) K J I g f) u) ∈ B)
11. (a1 I (cat-id(C) I)) = (a2 I (cat-id(C) I)) ∈ (A ⟶ B)
12. J : cat-ob(C)
13. f : cat-arrow(C) J I
14. u : discr(A)(f(a))
15. (a1 I (cat-id(C) I) u) = (a2 I (cat-id(C) I) u) ∈ B
⊢ discr(B)(f(a)) = B ∈ Type
BY
{ Computation }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  C  :  SmallCategory
2.  A  :  Type
3.  B  :  Type
4.  X  :  ps\_context\{j:l\}(C)
5.  I  :  cat-ob(C)
6.  a  :  X(I)
7.  a1  :  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B
8.  \mforall{}J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}u:A.
          ((a1  J  f  u)  =  (a1  K  (cat-comp(C)  K  J  I  g  f)  u))
9.  a2  :  J:cat-ob(C)  {}\mrightarrow{}  f:(cat-arrow(C)  J  I)  {}\mrightarrow{}  u:A  {}\mrightarrow{}  B
10.  \mforall{}J,K:cat-ob(C).  \mforall{}f:cat-arrow(C)  J  I.  \mforall{}g:cat-arrow(C)  K  J.  \mforall{}u:A.
            ((a2  J  f  u)  =  (a2  K  (cat-comp(C)  K  J  I  g  f)  u))
11.  (a1  I  (cat-id(C)  I))  =  (a2  I  (cat-id(C)  I))
12.  J  :  cat-ob(C)
13.  f  :  cat-arrow(C)  J  I
14.  u  :  discr(A)(f(a))
15.  (a1  I  (cat-id(C)  I)  u)  =  (a2  I  (cat-id(C)  I)  u)
\mvdash{}  discr(B)(f(a))  =  B


By

---

Latex:
Computation

---

Home Index