Step
*
2
2
1
1
1
of Lemma
functor-curry-iso
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ (arrow(functor-comp(functor-uncurry(C);functor-curry(A;B))) x y f A1)
= (f A1)
∈ nat-trans(B;C;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x)
A1;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1)
BY
{ BLemma `nat-trans-equal2` }
1
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ B ∈ SmallCategory
2
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ C ∈ SmallCategory
3
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) A1 ∈ Functor(B;C)
4
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1 ∈ Functor(B;C)
5
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ arrow(functor-comp(functor-uncurry(C);functor-curry(A;B))) x y f A1
∈ nat-trans(B;C;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x)
A1;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1)
6
.....wf.....
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ f A1 ∈ nat-trans(B;C;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x)
A1;ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1)
7
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) ∈ Functor(FUN(A;FUN(B;C));FUN(A × B;C))
5. functor-curry(A;B) ∈ Functor(FUN(A × B;C);FUN(A;FUN(B;C)))
6. ∀x:Functor(A × B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C))
7. ∀f:Functor(A;FUN(B;C)). ∀a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1
9. ∀x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x ∈ Functor(A;FUN(B;C)))
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
⊢ (arrow(functor-comp(functor-uncurry(C);functor-curry(A;B))) x y f A1)
= (f A1)
∈ (A2:cat-ob(B) ⟶ (cat-arrow(C) (ob(ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) A1) A2)
(ob(ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) y) A1) A2)))
Latex:
Latex:
1. A : SmallCategory
2. B : SmallCategory
3. C : SmallCategory
4. functor-uncurry(C) \mmember{} Functor(FUN(A;FUN(B;C));FUN(A \mtimes{} B;C))
5. functor-curry(A;B) \mmember{} Functor(FUN(A \mtimes{} B;C);FUN(A;FUN(B;C)))
6. \mforall{}x:Functor(A \mtimes{} B;C). ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x)
7. \mforall{}f:Functor(A;FUN(B;C)). \mforall{}a:cat-ob(A).
((ob(ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) f) a) = (ob(f) a))
8. functor-curry(A;B)functor-uncurry(C)=1
9. \mforall{}x:Functor(A;FUN(B;C)). ((ob(functor-comp(functor-uncurry(C);functor-curry(A;B))) x) = x)
10. x : Functor(A;FUN(B;C))
11. y : Functor(A;FUN(B;C))
12. f : nat-trans(A;FUN(B;C);x;y)
13. A1 : cat-ob(A)
\mvdash{} (arrow(functor-comp(functor-uncurry(C);functor-curry(A;B))) x y f A1) = (f A1)
By
Latex:
BLemma `nat-trans-equal2`
Home
Index