Step * 1 1 of Lemma functor-curry-iso


1. SmallCategory@i'
2. SmallCategory@i'
3. 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)) a) (f a) ∈ cat-ob(FUN(B;C)))
8. Functor(A × B;C)@i
9. Functor(A × B;C)@i
10. nat-trans(A × B;C;x;y)@i
⊢ (functor-comp(functor-curry(A;B);functor-uncurry(C)) f)
f
∈ nat-trans(A × B;C;functor-comp(functor-curry(A;B);functor-uncurry(C)) x;functor-comp(functor-curry(A;B);
                                                                                       functor-uncurry(C)) 
                                                                          y)
BY
(BLemma `nat-trans-equal2` THENW (Try ((InferEqualType THEN Try (Trivial) THEN RWO  "6" 0  THEN Auto)) THEN Auto)) }

1
1. SmallCategory@i'
2. SmallCategory@i'
3. 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)) a) (f a) ∈ cat-ob(FUN(B;C)))
8. Functor(A × B;C)@i
9. Functor(A × B;C)@i
10. nat-trans(A × B;C;x;y)@i
⊢ (functor-comp(functor-curry(A;B);functor-uncurry(C)) f)
f
∈ (A1:cat-ob(A × B) ⟶ (cat-arrow(C) (functor-comp(functor-curry(A;B);functor-uncurry(C)) A1) 
                        (functor-comp(functor-curry(A;B);functor-uncurry(C)) A1)))


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.  x  :  Functor(A  \mtimes{}  B;C)@i
9.  y  :  Functor(A  \mtimes{}  B;C)@i
10.  f  :  nat-trans(A  \mtimes{}  B;C;x;y)@i
\mvdash{}  (functor-comp(functor-curry(A;B);functor-uncurry(C))  x  y  f)  =  f


By


Latex:
(BLemma  `nat-trans-equal2`
  THENW  (Try  ((InferEqualType  THEN  Try  (Trivial)  THEN  RWO    "6"  0    THEN  Auto))  THEN  Auto)
  )




Home Index