Step
*
1
2
of Lemma
equal-monads
.....subterm..... T:t
2:n
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : nat-trans(C;C;functor-comp(T1;T1);T1)
5. (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (M7 (T1 X)) (M8 X)) = (cat-id(C) (T1 X)) ∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (T1 X (T1 X) (M7 X)) (M8 X))
= (cat-id(C) (T1 X))
∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (M8 (T1 X)) (M8 X))
= (cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (T1 (T1 (T1 X)) (T1 X) (M8 X)) (M8 X))
∈ (cat-arrow(C) (T1 (T1 (T1 X))) (T1 X))))
6. T : Functor(C;C)
7. M5 : nat-trans(C;C;1;T)
8. M6 : nat-trans(C;C;functor-comp(T;T);T)
9. (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (M5 (T X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M5 X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M6 (T X)) (M6 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M6 X)) (M6 X))
∈ (cat-arrow(C) (T (T (T X))) (T X))))
10. T1 = T ∈ Functor(C;C)
11. ∀x:cat-ob(C). ((T1 x) = (T x) ∈ cat-ob(C))
12. ∀x:cat-ob(C). ((M7 x) = (M5 x) ∈ (cat-arrow(C) x (T1 x)))
13. ∀x:cat-ob(C). ((M8 x) = (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
⊢ M8 = M6 ∈ nat-trans(C;C;functor-comp(T1;T1);T1)
BY
{ (DVar `M8' THEN EqTypeCD THEN Try (Trivial) THEN Try ((Fold `member` 0 THEN Auto))) }
1
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : A:cat-ob(C) ⟶ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 A))
5. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(C) (functor-comp(T1;T1) A) (T1 A) (T1 B) (M8 A) (T1 A B g))
= (cat-comp(C) (functor-comp(T1;T1) A) (functor-comp(T1;T1) B) (T1 B) (functor-comp(T1;T1) A B g) (M8 B))
∈ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 B)))
6. (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (M7 (T1 X)) (M8 X)) = (cat-id(C) (T1 X)) ∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (T1 X (T1 X) (M7 X)) (M8 X))
= (cat-id(C) (T1 X))
∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (M8 (T1 X)) (M8 X))
= (cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (T1 (T1 (T1 X)) (T1 X) (M8 X)) (M8 X))
∈ (cat-arrow(C) (T1 (T1 (T1 X))) (T1 X))))
7. T : Functor(C;C)
8. M5 : nat-trans(C;C;1;T)
9. M6 : nat-trans(C;C;functor-comp(T;T);T)
10. (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (M5 (T X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M5 X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M6 (T X)) (M6 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M6 X)) (M6 X))
∈ (cat-arrow(C) (T (T (T X))) (T X))))
11. T1 = T ∈ Functor(C;C)
12. ∀x:cat-ob(C). ((T1 x) = (T x) ∈ cat-ob(C))
13. ∀x:cat-ob(C). ((M7 x) = (M5 x) ∈ (cat-arrow(C) x (T1 x)))
14. ∀x:cat-ob(C). ((M8 x) = (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
⊢ M8 = M6 ∈ (A:cat-ob(C) ⟶ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 A)))
2
.....wf.....
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : A:cat-ob(C) ⟶ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 A))
5. ∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(C) (functor-comp(T1;T1) A) (T1 A) (T1 B) (M8 A) (T1 A B g))
= (cat-comp(C) (functor-comp(T1;T1) A) (functor-comp(T1;T1) B) (T1 B) (functor-comp(T1;T1) A B g) (M8 B))
∈ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 B)))
6. (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (M7 (T1 X)) (M8 X)) = (cat-id(C) (T1 X)) ∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (T1 X (T1 X) (M7 X)) (M8 X))
= (cat-id(C) (T1 X))
∈ (cat-arrow(C) (T1 X) (T1 X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (M8 (T1 X)) (M8 X))
= (cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (T1 (T1 (T1 X)) (T1 X) (M8 X)) (M8 X))
∈ (cat-arrow(C) (T1 (T1 (T1 X))) (T1 X))))
7. T : Functor(C;C)
8. M5 : nat-trans(C;C;1;T)
9. M6 : nat-trans(C;C;functor-comp(T;T);T)
10. (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (M5 (T X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M5 X)) (M6 X)) = (cat-id(C) (T X)) ∈ (cat-arrow(C) (T X) (T X))))
∧ (∀X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M6 (T X)) (M6 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M6 X)) (M6 X))
∈ (cat-arrow(C) (T (T (T X))) (T X))))
11. T1 = T ∈ Functor(C;C)
12. ∀x:cat-ob(C). ((T1 x) = (T x) ∈ cat-ob(C))
13. ∀x:cat-ob(C). ((M7 x) = (M5 x) ∈ (cat-arrow(C) x (T1 x)))
14. ∀x:cat-ob(C). ((M8 x) = (M6 x) ∈ (cat-arrow(C) (T1 (T1 x)) (T1 x)))
15. trans : A:cat-ob(C) ⟶ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 A))
⊢ istype(∀A,B:cat-ob(C). ∀g:cat-arrow(C) A B.
((cat-comp(C) (functor-comp(T1;T1) A) (T1 A) (T1 B) (trans A) (T1 A B g))
= (cat-comp(C) (functor-comp(T1;T1) A) (functor-comp(T1;T1) B) (T1 B) (functor-comp(T1;T1) A B g) (trans B))
∈ (cat-arrow(C) (functor-comp(T1;T1) A) (T1 B))))
Latex:
Latex:
.....subterm..... T:t
2:n
1. C : SmallCategory
2. T1 : Functor(C;C)
3. M7 : nat-trans(C;C;1;T1)
4. M8 : nat-trans(C;C;functor-comp(T1;T1);T1)
5. (\mforall{}X:cat-ob(C). ((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (M7 (T1 X)) (M8 X)) = (cat-id(C) (T1 X))))
\mwedge{} (\mforall{}X:cat-ob(C)
((cat-comp(C) (T1 X) (T1 (T1 X)) (T1 X) (T1 X (T1 X) (M7 X)) (M8 X)) = (cat-id(C) (T1 X))))
\mwedge{} (\mforall{}X:cat-ob(C)
((cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (M8 (T1 X)) (M8 X))
= (cat-comp(C) (T1 (T1 (T1 X))) (T1 (T1 X)) (T1 X) (T1 (T1 (T1 X)) (T1 X) (M8 X)) (M8 X))))
6. T : Functor(C;C)
7. M5 : nat-trans(C;C;1;T)
8. M6 : nat-trans(C;C;functor-comp(T;T);T)
9. (\mforall{}X:cat-ob(C). ((cat-comp(C) (T X) (T (T X)) (T X) (M5 (T X)) (M6 X)) = (cat-id(C) (T X))))
\mwedge{} (\mforall{}X:cat-ob(C)
((cat-comp(C) (T X) (T (T X)) (T X) (T X (T X) (M5 X)) (M6 X)) = (cat-id(C) (T X))))
\mwedge{} (\mforall{}X:cat-ob(C)
((cat-comp(C) (T (T (T X))) (T (T X)) (T X) (M6 (T X)) (M6 X))
= (cat-comp(C) (T (T (T X))) (T (T X)) (T X) (T (T (T X)) (T X) (M6 X)) (M6 X))))
10. T1 = T
11. \mforall{}x:cat-ob(C). ((T1 x) = (T x))
12. \mforall{}x:cat-ob(C). ((M7 x) = (M5 x))
13. \mforall{}x:cat-ob(C). ((M8 x) = (M6 x))
\mvdash{} M8 = M6
By
Latex:
(DVar `M8' THEN EqTypeCD THEN Try (Trivial) THEN Try ((Fold `member` 0 THEN Auto)))
Home
Index