---

Step * of Lemma psdcff-inj-injection

No Annotations
∀[C:SmallCategory]. ∀[A,B:Type]. ∀[X:ps_context{j:l}(C)]. ∀[I:cat-ob(C)]. ∀[a:X(I)].
  Inj(presheaf-fun-family(C; X; discr(A); discr(B); I; a);A ⟶ B;λw.psdcff-inj(I;w))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN D -3
   THEN (EqTypeCD THENW Auto)
   THEN Try (Trivial)
   THEN (D -2 THEN ∀h:hyp. RepUR ``discrete-presheaf-type psdcff-inj`` h )
   THEN RepeatFor 3 ((FunExt THENA Auto))) }

1
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))
⊢ (a1 J f u) = (a2 J f u) ∈ discr(B)(f(a))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[A,B:Type].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[I:cat-ob(C)].  \mforall{}[a:X(I)].
    Inj(presheaf-fun-family(C;  X;  discr(A);  discr(B);  I;  a);A  {}\mrightarrow{}  B;\mlambda{}w.psdcff-inj(I;w))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  D  -3
  THEN  (EqTypeCD  THENW  Auto)
  THEN  Try  (Trivial)
  THEN  (D  -2  THEN  \mforall{}h:hyp.  RepUR  ``discrete-presheaf-type  psdcff-inj``  h  )
  THEN  RepeatFor  3  ((FunExt  THENA  Auto)))

---

Home Index