Step
*
1
of Lemma
psdcff-inj-injection
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))
BY
{ ((ApFunToHypEquands `Z' ⌜Z u⌝ ⌜B⌝ (-4)⋅ THENA Auto) THEN Reduce -1 THEN NthHypEq (-1) THEN EqCDA) }
1
.....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
2
.....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))
3
.....subterm..... T:t
3: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
⊢ (a2 J f u) = (a2 I (cat-id(C) I) u) ∈ discr(B)(f(a))
Latex:
Latex:
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))
\mvdash{} (a1 J f u) = (a2 J f u)
By
Latex:
((ApFunToHypEquands `Z' \mkleeneopen{}Z u\mkleeneclose{} \mkleeneopen{}B\mkleeneclose{} (-4)\mcdot{} THENA Auto) THEN Reduce -1 THEN NthHypEq (-1) THEN EqCDA)
Home
Index