---

Step * 1 2 of Lemma psdcff-inj-injection

.....subterm..... T:t
2: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
⊢ (a1 J f u) = (a1 I (cat-id(C) I) u) ∈ discr(B)(f(a))
BY
{ OnMaybeHyp 8 (\h. ((InstHyp [⌜I⌝;⌜J⌝;⌜cat-id(C) I⌝;⌜f⌝;⌜u⌝] h⋅ THENA Auto)
                     THEN Symmetry
                     THEN NthHypEq (-1)
                     THEN EqCD
                     THEN Complete (Auto))) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2: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{}  (a1  J  f  u)  =  (a1  I  (cat-id(C)  I)  u)


By

---

Latex:
OnMaybeHyp  8  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}cat-id(C)  I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]  h\mcdot{}  THENA  Auto)
                                      THEN  Symmetry
                                      THEN  NthHypEq  (-1)
                                      THEN  EqCD
                                      THEN  Complete  (Auto)))

---

Home Index