Step * of Lemma functor-curry-iso

`No Annotations`
`∀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)`
`                   ((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).`
`                   ((functor-comp(functor-uncurry(C);functor-curry(A;B)) f a) = (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@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)))`
`⊢ functor-comp(functor-curry(A;B);functor-uncurry(C)) = 1 ∈ Functor(FUN(A × B;C);FUN(A × B;C))`

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

Latex:

Latex:
No  Annotations
\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).  ((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).
((functor-comp(functor-uncurry(C);functor-curry(A;B))  f  a)  =  (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