---

Step * of Lemma functor-curry-iso

∀A,B,C:SmallCategory.  cat-isomorphic(Cat;FUN(A × B;C);FUN(A;FUN(B;C)))
BY
{ (((Auto
     THEN (InstLemma `functor-uncurry_wf` [⌜A⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto)
     THEN (InstLemma `functor-curry_wf` [⌜A⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto))
    THEN (Assert ∀x:Functor(A × B;C)
                   ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C))) x) = x ∈ Functor(A × B;C)) BY
                (Auto
                 THEN (((BLemma `equal-functors` THENW Auto) THEN Intros)
                       THENL [(D -1 THEN RepUR ``functor-comp functor-uncurry functor-curry`` 0 THEN Auto)
                             ; ((All Reduce THEN DProds)
                                THEN RepUR ``functor-comp functor-uncurry functor-curry`` 0
                                THEN RW CatNormC 0
                                THEN Auto)]
                      )
                 ))
    THEN (Assert ∀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))) BY
                ((Auto THEN All Reduce THEN (BLemma `equal-functors` THENW Auto) THEN Intros)
                 THENL [(RepUR ``functor-comp functor-uncurry functor-curry`` 0 THEN Auto)
                       ; (RepUR ``functor-comp functor-uncurry functor-curry`` 0 THEN RW CatNormC 0 THEN Auto)]
                )))
   THEN (D 0 With ⌜functor-curry(A;B)⌝  THENW (Auto THEN RepUR ``cat-ob cat-cat`` 0 THEN Auto))
   THEN D 0 With ⌜functor-uncurry(C)⌝ 
   THEN Auto
   THEN Try ((RepUR ``cat-cat`` 0 THEN Complete (Auto)))
   THEN RepUR ``cat-inverse cat-cat`` 0) }

1
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)))
⊢ functor-comp(functor-curry(A;B);functor-uncurry(C)) = 1 ∈ Functor(FUN(A × B;C);FUN(A × B;C))

2
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
⊢ functor-comp(functor-uncurry(C);functor-curry(A;B)) = 1 ∈ Functor(FUN(A;FUN(B;C));FUN(A;FUN(B;C)))

---

Latex:

---

Latex:
\mforall{}A,B,C:SmallCategory.    cat-isomorphic(Cat;FUN(A  \mtimes{}  B;C);FUN(A;FUN(B;C)))


By

---

Latex:
(((Auto
      THEN  (InstLemma  `functor-uncurry\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
      THEN  (InstLemma  `functor-curry\_wf`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto))
    THEN  (Assert  \mforall{}x:Functor(A  \mtimes{}  B;C)
                                  ((ob(functor-comp(functor-curry(A;B);functor-uncurry(C)))  x)  =  x)  BY
                            (Auto
                              THEN  (((BLemma  `equal-functors`  THENW  Auto)  THEN  Intros)
                                          THENL  [(D  -1
                                                          THEN  RepUR  ``functor-comp  functor-uncurry  functor-curry``  0
                                                          THEN  Auto)
                                                      ;  ((All  Reduce  THEN  DProds)
                                                            THEN  RepUR  ``functor-comp  functor-uncurry  functor-curry``  0
                                                            THEN  RW  CatNormC  0
                                                            THEN  Auto)]
                                        )
                              ))
    THEN  (Assert  \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))  BY
                            ((Auto  THEN  All  Reduce  THEN  (BLemma  `equal-functors`  THENW  Auto)  THEN  Intros)
                              THENL  [(RepUR  ``functor-comp  functor-uncurry  functor-curry``  0  THEN  Auto)
                                          ;  (RepUR  ``functor-comp  functor-uncurry  functor-curry``  0
                                                THEN  RW  CatNormC  0
                                                THEN  Auto)]
                            )))
  THEN  (D  0  With  \mkleeneopen{}functor-curry(A;B)\mkleeneclose{}    THENW  (Auto  THEN  RepUR  ``cat-ob  cat-cat``  0  THEN  Auto))
  THEN  D  0  With  \mkleeneopen{}functor-uncurry(C)\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((RepUR  ``cat-cat``  0  THEN  Complete  (Auto)))
  THEN  RepUR  ``cat-inverse  cat-cat``  0)

---

Home Index