Proof of Nuprl Lemma : functor-curry-iso

Step * 2 2 1 1 1 of Lemma functor-curry-iso

1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ (functor-comp(functor-uncurry(C);functor-curry(A;B)) x y f A1)
= (f A1)
∈ nat-trans(B;C;functor-comp(functor-uncurry(C);functor-curry(A;B)) x A1;functor-comp(functor-uncurry(C);

                                                                                      functor-curry(A;B))

A1)

BY
{ BLemma `nat-trans-equal2` }

1
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ B ∈ SmallCategory

2
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ C ∈ SmallCategory

3
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ functor-comp(functor-uncurry(C);functor-curry(A;B)) x A1 ∈ Functor(B;C)

4
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ functor-comp(functor-uncurry(C);functor-curry(A;B)) y A1 ∈ Functor(B;C)

5
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ functor-comp(functor-uncurry(C);functor-curry(A;B)) x y f A1
∈ nat-trans(B;C;functor-comp(functor-uncurry(C);functor-curry(A;B)) x A1;functor-comp(functor-uncurry(C);

                                                                                        functor-curry(A;B))

A1)

6
.....wf.....
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ f A1 ∈ nat-trans(B;C;functor-comp(functor-uncurry(C);functor-curry(A;B)) x
A1;functor-comp(functor-uncurry(C);functor-curry(A;B)) y A1)

7
1. A : SmallCategory@i'
2. B : SmallCategory@i'
3. C : SmallCategory@i'
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). ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a) ∈ cat-ob(FUN(B;C)))
8. functor-curry(A;B)functor-uncurry(C)=1

9. ∀x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x ∈ Functor(A;FUN(B;C)))

10. x : Functor(A;FUN(B;C))@i
11. y : Functor(A;FUN(B;C))@i
12. f : nat-trans(A;FUN(B;C);x;y)@i
13. A1 : cat-ob(A)
⊢ (functor-comp(functor-uncurry(C);functor-curry(A;B)) x y f A1)
= (f A1)
∈ (A2:cat-ob(B) ⟶ (cat-arrow(C) (functor-comp(functor-uncurry(C);functor-curry(A;B)) x A1 A2)
(functor-comp(functor-uncurry(C);functor-curry(A;B)) y A1 A2)))

Latex:

Latex:
1. A : SmallCategory@i' 2. B : SmallCategory@i' 3. C : SmallCategory@i' 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). ((functor-comp(functor-curry(A;B);functor-uncurry(C)) x) = x) 7. \mforall{}f:Functor(A;FUN(B;C)). \mforall{}a:cat-ob(A). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (f a)) 8. functor-curry(A;B)functor-uncurry(C)=1 9. \mforall{}x:Functor(A;FUN(B;C)). ((functor-comp(functor-uncurry(C);functor-curry(A;B)) x) = x) 10. x : Functor(A;FUN(B;C))@i 11. y : Functor(A;FUN(B;C))@i 12. f : nat-trans(A;FUN(B;C);x;y)@i 13. A1 : cat-ob(A) \mvdash{} (functor-comp(functor-uncurry(C);functor-curry(A;B)) x y f A1) = (f A1) By Latex: BLemma `nat-trans-equal2` Home Index