From 0484b6f03102269b8dbd015e9956b3f7ad303164 Mon Sep 17 00:00:00 2001
From: Marco Perone <pasafama@gmail.com>
Date: Mon, 3 Jun 2019 08:42:59 +0200
Subject: [PATCH 01/13] split TerminalObject and Product into separate files

---
 src/Limits/Product.lidr        | 47 ++++++++++++++++++++++++++++++++++
 src/Limits/TerminalObject.lidr | 33 ++++++++++++++++++++++++
 2 files changed, 80 insertions(+)
 create mode 100644 src/Limits/Product.lidr
 create mode 100644 src/Limits/TerminalObject.lidr

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
new file mode 100644
index 0000000..cbac7b7
--- /dev/null
+++ b/src/Limits/Product.lidr
@@ -0,0 +1,47 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Limits.Product
+>
+> import Basic.Category
+>
+> %access public export
+> %default total
+> %auto_implicits off
+>
+> record CommutingMorphism (cat : Category)
+>                          (x : obj cat) (a : obj cat) (b : obj cat) (carrier : obj cat)
+>                          (pi1 : mor cat carrier a) (pi2 : mor cat carrier b)
+>                          (f : mor cat x a) (g : mor cat x b) where
+>   constructor MkCommutingMorphism
+>   challenger         : mor cat x carrier
+>   commutativityLeft  : compose cat x carrier a challenger pi1 = f
+>   commutativityRight : compose cat x carrier b challenger pi2 = g
+>
+> record Product (cat : Category) (a : obj cat) (b : obj cat) where
+>   constructor MkProduct
+>   carrier : obj cat
+>   pi1 : mor cat carrier a
+>   pi2 : mor cat carrier b
+>   exists : (x : obj cat) -> (f : mor cat x a) -> (g : mor cat x b) -> CommutingMorphism cat x a b carrier pi1 pi2 f g
+>   unique : (x : obj cat) -> (f : mor cat x a) -> (g : mor cat x b)
+>         -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
+>         -> h = exists x f g
diff --git a/src/Limits/TerminalObject.lidr b/src/Limits/TerminalObject.lidr
new file mode 100644
index 0000000..0401ba3
--- /dev/null
+++ b/src/Limits/TerminalObject.lidr
@@ -0,0 +1,33 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Limits.TerminalObject
+>
+> import Basic.Category
+>
+> %access public export
+> %default total
+>
+> record TerminalObject (cat : Category) where
+>   constructor MkTerminalObject
+>   carrier : obj cat
+>   exists  : (a : obj cat) -> mor cat a carrier
+>   unique  : (a : obj cat) -> (f : mor cat a carrier) -> f = exists a

From 794372fabe2bb5cdc8b78466e8867d8889b550f4 Mon Sep 17 00:00:00 2001
From: Marco Perone <pasafama@gmail.com>
Date: Tue, 4 Jun 2019 17:48:20 +0200
Subject: [PATCH 02/13] prove that terminal objects are isomorphic

---
 src/Limits/TerminalObject.lidr | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Limits/TerminalObject.lidr b/src/Limits/TerminalObject.lidr
index 0401ba3..1d5f28f 100644
--- a/src/Limits/TerminalObject.lidr
+++ b/src/Limits/TerminalObject.lidr
@@ -22,6 +22,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > module Limits.TerminalObject
 >
 > import Basic.Category
+> import Basic.Isomorphism
 >
 > %access public export
 > %default total
@@ -30,4 +31,20 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >   constructor MkTerminalObject
 >   carrier : obj cat
 >   exists  : (a : obj cat) -> mor cat a carrier
->   unique  : (a : obj cat) -> (f : mor cat a carrier) -> f = exists a
+>   unique  : (a : obj cat) -> (f, g : mor cat a carrier) -> f = g
+>
+> composeTerminalMorphisms :
+>      (cat : Category)
+>   -> (a, b : TerminalObject cat)
+>   -> mor cat (carrier a) (carrier a)
+> composeTerminalMorphisms cat a b =
+>   compose cat (carrier a) (carrier b) (carrier a) (exists b (carrier a)) (exists a (carrier b))
+>
+> terminalObjectsAreIsomorphic :
+>      (cat : Category)
+>   -> (a, b : TerminalObject cat)
+>   -> Isomorphism cat (carrier a) (carrier b) (exists b (carrier a))
+> terminalObjectsAreIsomorphic cat a b = MkIsomorphism
+>   (exists a (carrier b))
+>   (unique a (carrier a) (composeTerminalMorphisms cat a b) (identity cat (carrier a)))
+>   (unique b (carrier b) (composeTerminalMorphisms cat b a) (identity cat (carrier b)))

From 34049f80d15659f3a2a24a8aefb4ccab2159fd14 Mon Sep 17 00:00:00 2001
From: liveshare <jelle@defekt.nl>
Date: Thu, 6 Jun 2019 14:46:29 +0000
Subject: [PATCH 03/13] live sharing session

---
 src/Limits/Product.lidr | 63 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index cbac7b7..c2353c2 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -22,6 +22,8 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > module Limits.Product
 >
 > import Basic.Category
+> import Basic.Functor
+> import Product.ProductCategory
 >
 > %access public export
 > %default total
@@ -45,3 +47,64 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >   unique : (x : obj cat) -> (f : mor cat x a) -> (g : mor cat x b)
 >         -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
 >         -> h = exists x f g
+>
+> productMorphism : (cat : Category) -> (a1, a2, b1, b2 : obj cat) 
+>                -> (f : mor cat a1 a2) -> (g : mor cat b1 b2) 
+>                -> (pr1 : Product cat a1 b1) -> (pr2 : Product cat a2 b2)
+>                -> mor cat (carrier pr1) (carrier pr2)
+> productMorphism cat a1 a2 b1 b2 f g pr1 pr2 = 
+>   challenger $ exists pr2 prod1 (compose cat _ _ _ pi1' f) (compose cat _ _ _ pi2' g)
+>     where
+>       prod1 : obj cat
+>       prod1 = carrier pr1
+>       prod2 : obj cat
+>       prod2 = carrier pr2
+>       pi1' : mor cat prod1 a1
+>       pi1' = pi1 pr1
+>       pi2' : mor cat prod1 b1
+>       pi2' = pi2 pr1
+> 
+> productFunctor : (cat : Category) -> (pex : (a, b : obj cat) -> Product cat a b) -> CFunctor (productCategory cat cat) cat
+> productFunctor cat pex = MkCFunctor mapObj mapMor idLaw ?compLaw
+>   where
+>     mapObj : obj (productCategory cat cat) -> obj cat
+>     mapObj (a,b) = carrier $ pex a b
+>     mapMor : (a, b : obj (productCategory cat cat))
+>            -> mor (productCategory cat cat) a b
+>            -> mor cat (mapObj a) (mapObj b)
+>     mapMor (a1,b1) (a2,b2) (MkProductMorphism f g) = 
+>       productMorphism cat a1 a2 b1 b2 f g (pex a1 b1) (pex a2 b2)
+>     bla : (a,b : obj cat) -> CommutingMorphism cat (carrier (pex a b)) a b (carrier (pex a b))
+>                              (pi1 (pex a b))
+>                              (pi2 (pex a b))
+>                              (compose cat (carrier (pex a b)) a a (pi1 (pex a b)) (identity cat a))
+>                              (compose cat (carrier (pex a b)) b b (pi2 (pex a b)) (identity cat b))
+>     bla a b = MkCommutingMorphism (identity cat (carrier (pex a b))) 
+>                            (rewrite leftIdentity cat (carrier (pex a b)) a (pi1 (pex a b)) in 
+>                             sym $ rightIdentity cat (carrier (pex a b)) a (pi1 (pex a b)))
+>                            (rewrite leftIdentity cat (carrier (pex a b)) b (pi2 (pex a b)) in
+>                             sym $ rightIdentity cat (carrier (pex a b)) b (pi2 (pex a b)))
+>     idLaw : (a : obj (productCategory cat cat)) -> mapMor a a (identity (productCategory cat cat) a) = identity cat (mapObj a)
+>     idLaw (a,b) = sym $ cong {f=challenger} $ 
+>                   unique (pex a b) (carrier (pex a b)) 
+>                          (compose cat (carrier (pex a b)) a a (pi1 (pex a b)) (identity cat a))
+>                          (compose cat (carrier (pex a b)) b b (pi2 (pex a b)) (identity cat b))
+>                          (bla a b) 
+>
+> catHasProducts : Category -> Type
+> catHasProducts cat = (a, b : obj cat) -> Product cat a b
+
+
+(AxB) x C --> A x (B x C)
+< pi1_{(AxB)xC};pi1_{AxB}, < pi1_{(AxB)xC};pi2_{AxB}, pi2_{(AxB)xC}> > 
+
+
+    MkCFunctor
+       (\(a, b) => carrier $ pex a b)
+       (\(a1, b1), (a2, b2), (f, g) => productMorphism cat a1 a2 b1 b2 f g (pex a1 b1) (pex a2 b2))
+       ?id
+       ?comp
+
+ catHasProducts : 
+
+exists_a2.b2 (pi1_a1.b1;f, pi2_a1.b1;g )
\ No newline at end of file

From daf49287cf865574b58921701a5aa5631217709e Mon Sep 17 00:00:00 2001
From: Marco Perone <pasafama@gmail.com>
Date: Mon, 10 Jun 2019 16:09:10 +0200
Subject: [PATCH 04/13] useless fixes

---
 src/CoLimits/CoProduct.lidr |   5 +-
 src/Limits/Product.lidr     | 128 ++++++++++++++++++------------------
 2 files changed, 64 insertions(+), 69 deletions(-)

diff --git a/src/CoLimits/CoProduct.lidr b/src/CoLimits/CoProduct.lidr
index 32d0003..7aa71c0 100644
--- a/src/CoLimits/CoProduct.lidr
+++ b/src/CoLimits/CoProduct.lidr
@@ -38,10 +38,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >   commutativityLeft  : compose cat a carrier c inl challenger = f
 >   commutativityRight : compose cat b carrier c inr challenger = g
 >
-> record CoProduct
->   (cat : Category)
->   (a : obj cat) (b : obj cat)
-> where
+> record CoProduct (cat : Category) (a : obj cat) (b : obj cat) where
 >   constructor MkCoProduct
 >   carrier: obj cat
 >   inl: mor cat a carrier
diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index c2353c2..af43718 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -29,10 +29,12 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > %default total
 > %auto_implicits off
 >
-> record CommutingMorphism (cat : Category)
->                          (x : obj cat) (a : obj cat) (b : obj cat) (carrier : obj cat)
->                          (pi1 : mor cat carrier a) (pi2 : mor cat carrier b)
->                          (f : mor cat x a) (g : mor cat x b) where
+> record CommutingMorphism
+>   (cat : Category)
+>   (x : obj cat) (a : obj cat) (b : obj cat) (carrier : obj cat)
+>   (pi1 : mor cat carrier a) (pi2 : mor cat carrier b)
+>   (f : mor cat x a) (g : mor cat x b)
+> where
 >   constructor MkCommutingMorphism
 >   challenger         : mor cat x carrier
 >   commutativityLeft  : compose cat x carrier a challenger pi1 = f
@@ -43,68 +45,64 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >   carrier : obj cat
 >   pi1 : mor cat carrier a
 >   pi2 : mor cat carrier b
->   exists : (x : obj cat) -> (f : mor cat x a) -> (g : mor cat x b) -> CommutingMorphism cat x a b carrier pi1 pi2 f g
->   unique : (x : obj cat) -> (f : mor cat x a) -> (g : mor cat x b)
->         -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
->         -> h = exists x f g
+>   exists :
+>        (x : obj cat)
+>     -> (f : mor cat x a)
+>     -> (g : mor cat x b)
+>     -> CommutingMorphism cat x a b carrier pi1 pi2 f g
+>   unique :
+>        (x : obj cat)
+>     -> (f : mor cat x a)
+>     -> (g : mor cat x b)
+>     -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
+>     -> challenger h = challenger (exists x f g)
 >
-> productMorphism : (cat : Category) -> (a1, a2, b1, b2 : obj cat) 
->                -> (f : mor cat a1 a2) -> (g : mor cat b1 b2) 
->                -> (pr1 : Product cat a1 b1) -> (pr2 : Product cat a2 b2)
->                -> mor cat (carrier pr1) (carrier pr2)
-> productMorphism cat a1 a2 b1 b2 f g pr1 pr2 = 
->   challenger $ exists pr2 prod1 (compose cat _ _ _ pi1' f) (compose cat _ _ _ pi2' g)
->     where
->       prod1 : obj cat
->       prod1 = carrier pr1
->       prod2 : obj cat
->       prod2 = carrier pr2
->       pi1' : mor cat prod1 a1
->       pi1' = pi1 pr1
->       pi2' : mor cat prod1 b1
->       pi2' = pi2 pr1
-> 
-> productFunctor : (cat : Category) -> (pex : (a, b : obj cat) -> Product cat a b) -> CFunctor (productCategory cat cat) cat
-> productFunctor cat pex = MkCFunctor mapObj mapMor idLaw ?compLaw
->   where
->     mapObj : obj (productCategory cat cat) -> obj cat
->     mapObj (a,b) = carrier $ pex a b
->     mapMor : (a, b : obj (productCategory cat cat))
->            -> mor (productCategory cat cat) a b
->            -> mor cat (mapObj a) (mapObj b)
->     mapMor (a1,b1) (a2,b2) (MkProductMorphism f g) = 
->       productMorphism cat a1 a2 b1 b2 f g (pex a1 b1) (pex a2 b2)
->     bla : (a,b : obj cat) -> CommutingMorphism cat (carrier (pex a b)) a b (carrier (pex a b))
->                              (pi1 (pex a b))
->                              (pi2 (pex a b))
->                              (compose cat (carrier (pex a b)) a a (pi1 (pex a b)) (identity cat a))
->                              (compose cat (carrier (pex a b)) b b (pi2 (pex a b)) (identity cat b))
->     bla a b = MkCommutingMorphism (identity cat (carrier (pex a b))) 
->                            (rewrite leftIdentity cat (carrier (pex a b)) a (pi1 (pex a b)) in 
->                             sym $ rightIdentity cat (carrier (pex a b)) a (pi1 (pex a b)))
->                            (rewrite leftIdentity cat (carrier (pex a b)) b (pi2 (pex a b)) in
->                             sym $ rightIdentity cat (carrier (pex a b)) b (pi2 (pex a b)))
->     idLaw : (a : obj (productCategory cat cat)) -> mapMor a a (identity (productCategory cat cat) a) = identity cat (mapObj a)
->     idLaw (a,b) = sym $ cong {f=challenger} $ 
->                   unique (pex a b) (carrier (pex a b)) 
->                          (compose cat (carrier (pex a b)) a a (pi1 (pex a b)) (identity cat a))
->                          (compose cat (carrier (pex a b)) b b (pi2 (pex a b)) (identity cat b))
->                          (bla a b) 
+> productMorphism :
+>      (cat : Category)
+>   -> (a1, a2, b1, b2 : obj cat)
+>   -> (f : mor cat a1 a2)
+>   -> (g : mor cat b1 b2)
+>   -> (pr1 : Product cat a1 b1)
+>   -> (pr2 : Product cat a2 b2)
+>   -> mor cat (carrier pr1) (carrier pr2)
+> productMorphism cat a1 a2 b1 b2 f g pr1 pr2 =
+>   challenger $ exists pr2 (carrier pr1) (compose cat _ _ _ (pi1 pr1) f) (compose cat _ _ _ (pi2 pr1) g)
 >
 > catHasProducts : Category -> Type
 > catHasProducts cat = (a, b : obj cat) -> Product cat a b
-
-
-(AxB) x C --> A x (B x C)
-< pi1_{(AxB)xC};pi1_{AxB}, < pi1_{(AxB)xC};pi2_{AxB}, pi2_{(AxB)xC}> > 
-
-
-    MkCFunctor
-       (\(a, b) => carrier $ pex a b)
-       (\(a1, b1), (a2, b2), (f, g) => productMorphism cat a1 a2 b1 b2 f g (pex a1 b1) (pex a2 b2))
-       ?id
-       ?comp
-
- catHasProducts : 
-
-exists_a2.b2 (pi1_a1.b1;f, pi2_a1.b1;g )
\ No newline at end of file
+>
+> productFunctor :
+>      (cat : Category)
+>   -> (productObj : catHasProducts cat)
+>   -> CFunctor (productCategory cat cat) cat
+> productFunctor cat productObj = MkCFunctor mapObj mapMor idLaw ?compLaw
+>   where
+>     mapObj : (obj cat, obj cat) -> obj cat
+>     mapObj (a,b) = carrier $ productObj a b
+>     mapMor :
+>          (a, b : obj (productCategory cat cat))
+>       -> mor (productCategory cat cat) a b
+>       -> mor cat (mapObj a) (mapObj b)
+>     mapMor (a1,b1) (a2,b2) (MkProductMorphism f g) =
+>       productMorphism cat a1 a2 b1 b2 f g (productObj a1 b1) (productObj a2 b2)
+>     identityCommutingMorphism :
+>          (a,b : obj cat)
+>       -> CommutingMorphism cat
+>                            (carrier (productObj a b)) a b (carrier (productObj a b))
+>                            (pi1 (productObj a b)) (pi2 (productObj a b))
+>                            (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
+>                            (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
+>     identityCommutingMorphism a b =
+>       MkCommutingMorphism (identity cat (carrier (productObj a b)))
+>                           (rewrite leftIdentity cat (carrier (productObj a b)) a (pi1 (productObj a b)) in
+>                             sym $ rightIdentity cat (carrier (productObj a b)) a (pi1 (productObj a b)))
+>                           (rewrite leftIdentity cat (carrier (productObj a b)) b (pi2 (productObj a b)) in
+>                             sym $ rightIdentity cat (carrier (productObj a b)) b (pi2 (productObj a b)))
+>     idLaw :
+>          (a : obj (productCategory cat cat))
+>       -> mapMor a a (identity (productCategory cat cat) a) = identity cat (mapObj a)
+>     idLaw (a,b) = sym $ unique (productObj a b)
+>                                (carrier (productObj a b))
+>                                (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
+>                                (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
+>                                (identityCommutingMorphism a b)

From f3454e7b08bdad179a7299817b86e6118ce2a5f8 Mon Sep 17 00:00:00 2001
From: liveshare <wires@liveshare.c.statebox-infra.internal>
Date: Thu, 13 Jun 2019 14:14:55 +0000
Subject: [PATCH 05/13] liveshare

---
 README.md               |  6 ++++
 src/Limits/Product.lidr | 72 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)

diff --git a/README.md b/README.md
index 4687bf3..de0c008 100644
--- a/README.md
+++ b/README.md
@@ -41,6 +41,12 @@ If you want a more detailed and slow introduction to the library, please have a
 - https://blog.statebox.org/concrete-categories-af444d5f055e
 - https://blog.statebox.org/fun-with-functors-95e4e8d60d87
 
+## Lauching a Nix Shell
+
+```
+nix-shell -A idris-ct
+```
+
 ## Nix build
 
 If you have [Nix](https://nixos.org/nix/) installed, you can build the project just by doing
diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index af43718..48eb72b 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -24,6 +24,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 > import Basic.Category
 > import Basic.Functor
 > import Product.ProductCategory
+> import Limits.TerminalObject
 >
 > %access public export
 > %default total
@@ -106,3 +107,74 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
 >                                (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
 >                                (identityCommutingMorphism a b)
+>
+
+ rhoUnitor 
+
+> catHasTerminalObj : Category -> Type
+> catHasTerminalObj = TerminalObject
+>
+> bifunctorLeft : (cat : Category) -> (fun : CFunctor (productCategory cat cat) cat) -> (b : obj cat) -> CFunctor cat cat
+> bifunctorLeft cat fun@(MkCFunctor mapObj mapMor pId pComp) b = MkCFunctor mapObj' mapMor' pId' pComp'
+>   where 
+>     mapObj' : obj cat -> obj cat
+>     mapObj' x = mapObj (x, b)
+>     mapMor' : (x, y : obj cat) -> mor cat x y -> mor cat (mapObj' x) (mapObj' y)
+>     mapMor' x y mor = mapMor (x, b) (y, b) (MkProductMorphism mor (identity cat b))
+>     pId' : (x : obj cat) -> mapMor (x, b) (x, b) (MkProductMorphism (identity cat x) (identity cat b)) = identity cat (mapObj (x, b))
+>     pId' x = pId (x, b)
+>     pComp' : (x, y, z : obj cat) -> (f : mor cat x y) -> (g : mor cat y z) 
+>           -> mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) (identity cat b))
+>            = compose cat (mapObj (x, b)) (mapObj (y, b)) (mapObj (z, b)) (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b))) (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))
+>     pComp' x y z f g = 
+>       replace {P=\q=>mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) q) = compose cat (mapObj (x, b)) (mapObj (y, b)) (mapObj (z, b)) (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b))) (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))} 
+>               (leftIdentity cat b b (identity cat b)) 
+>               (pComp (x,b) (y,b) (z,b) (MkProductMorphism f (identity cat b)) (MkProductMorphism g (identity cat b)))
+
+Andre: seems like I got disconnected from the call and now nothing loads...
+We can read you tho, try reconnecting on zoom!
+use the link nin the issue?
+use the force!
+I'm so confused: zoom doesn't work in chrome and safari, and rocketchat is also not connecting, but I can view twitch just fine...
+Oldest trick in the world: Reboot
+I
+
+wth @andreK ???
+
+
+
+
+id_b ; id_b --> idb
+
+
+(-,b) --> (-,b)
+
+(id_a,id_b) --> id_{a x b}
+
+
+cat x cat -F-> cat 
+
+
+
+fun (a,b)
+     MkCFunctor ?mo ?mm ?pid ?pco
+
+> parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
+>   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
+>   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
+
+
+rightUnitor: ( - ) x 1 --> id cat
+
+rightUnitor_A : A x 1 -- pi1 -> A
+
+A x 1 --- pi1 ---> A
+    |                        |
+    |                        |
+  <pi1;f , pi2>      f
+    |                        |
+    |                       \ /
+B x 1 --- pi1 ---> B
+
+
+<pi1,pi2> = id_{AxB}
\ No newline at end of file

From ae5b64676ba95ab576645c1b94659e9d97980e36 Mon Sep 17 00:00:00 2001
From: Marco Perone <pasafama@gmail.com>
Date: Mon, 17 Jun 2019 12:53:02 +0200
Subject: [PATCH 06/13] clean code of shared coding session

---
 src/Limits/Product.lidr | 91 +++++++++++++++--------------------------
 1 file changed, 33 insertions(+), 58 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 48eb72b..a67bfc3 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -108,73 +108,48 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
 >                                (identityCommutingMorphism a b)
 >
-
- rhoUnitor 
-
 > catHasTerminalObj : Category -> Type
 > catHasTerminalObj = TerminalObject
 >
-> bifunctorLeft : (cat : Category) -> (fun : CFunctor (productCategory cat cat) cat) -> (b : obj cat) -> CFunctor cat cat
-> bifunctorLeft cat fun@(MkCFunctor mapObj mapMor pId pComp) b = MkCFunctor mapObj' mapMor' pId' pComp'
->   where 
+> bifunctorLeft :
+>      (cat : Category)
+>   -> (fun : CFunctor (productCategory cat cat) cat)
+>   -> (b : obj cat)
+>   -> CFunctor cat cat
+> bifunctorLeft cat (MkCFunctor mapObj mapMor pId pComp) b = MkCFunctor mapObj' mapMor' pId' pComp'
+>   where
 >     mapObj' : obj cat -> obj cat
 >     mapObj' x = mapObj (x, b)
+>
 >     mapMor' : (x, y : obj cat) -> mor cat x y -> mor cat (mapObj' x) (mapObj' y)
 >     mapMor' x y mor = mapMor (x, b) (y, b) (MkProductMorphism mor (identity cat b))
->     pId' : (x : obj cat) -> mapMor (x, b) (x, b) (MkProductMorphism (identity cat x) (identity cat b)) = identity cat (mapObj (x, b))
+>
+>     pId' :
+>          (x : obj cat)
+>       -> mapMor (x, b) (x, b) (MkProductMorphism (identity cat x) (identity cat b))
+>        = identity cat (mapObj (x, b))
 >     pId' x = pId (x, b)
->     pComp' : (x, y, z : obj cat) -> (f : mor cat x y) -> (g : mor cat y z) 
->           -> mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) (identity cat b))
->            = compose cat (mapObj (x, b)) (mapObj (y, b)) (mapObj (z, b)) (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b))) (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))
->     pComp' x y z f g = 
->       replace {P=\q=>mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) q) = compose cat (mapObj (x, b)) (mapObj (y, b)) (mapObj (z, b)) (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b))) (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))} 
->               (leftIdentity cat b b (identity cat b)) 
+>
+>     pComp' :
+>          (x, y, z : obj cat)
+>       -> (f : mor cat x y)
+>       -> (g : mor cat y z)
+>       -> mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) (identity cat b))
+>        = compose cat (mapObj (x, b))
+>                      (mapObj (y, b))
+>                      (mapObj (z, b))
+>                      (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b)))
+>                      (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))
+>     pComp' x y z f g =
+>       replace {P=\q => mapMor (x, b) (z, b) (MkProductMorphism (compose cat x y z f g) q)
+>                      = compose cat (mapObj (x, b))
+>                                    (mapObj (y, b))
+>                                    (mapObj (z, b))
+>                                    (mapMor (x, b) (y, b) (MkProductMorphism f (identity cat b)))
+>                                    (mapMor (y, b) (z, b) (MkProductMorphism g (identity cat b)))}
+>               (leftIdentity cat b b (identity cat b))
 >               (pComp (x,b) (y,b) (z,b) (MkProductMorphism f (identity cat b)) (MkProductMorphism g (identity cat b)))
-
-Andre: seems like I got disconnected from the call and now nothing loads...
-We can read you tho, try reconnecting on zoom!
-use the link nin the issue?
-use the force!
-I'm so confused: zoom doesn't work in chrome and safari, and rocketchat is also not connecting, but I can view twitch just fine...
-Oldest trick in the world: Reboot
-I
-
-wth @andreK ???
-
-
-
-
-id_b ; id_b --> idb
-
-
-(-,b) --> (-,b)
-
-(id_a,id_b) --> id_{a x b}
-
-
-cat x cat -F-> cat 
-
-
-
-fun (a,b)
-     MkCFunctor ?mo ?mm ?pid ?pco
-
+>
 > parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
 >   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
 >   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
-
-
-rightUnitor: ( - ) x 1 --> id cat
-
-rightUnitor_A : A x 1 -- pi1 -> A
-
-A x 1 --- pi1 ---> A
-    |                        |
-    |                        |
-  <pi1;f , pi2>      f
-    |                        |
-    |                       \ /
-B x 1 --- pi1 ---> B
-
-
-<pi1,pi2> = id_{AxB}
\ No newline at end of file

From 569595b558addeaa2779f8a4396396ef1c142103 Mon Sep 17 00:00:00 2001
From: liveshare <jelle@defekt.nl>
Date: Thu, 20 Jun 2019 14:48:04 +0000
Subject: [PATCH 07/13] liveshare

---
 src/Limits/Product.lidr        | 130 ++++++++++++++++++++++++++++++++-
 src/Limits/TerminalObject.lidr |  18 ++---
 2 files changed, 136 insertions(+), 12 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index a67bfc3..619276b 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -23,6 +23,9 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > import Basic.Category
 > import Basic.Functor
+> import Basic.Isomorphism
+> import Basic.NaturalTransformation
+> import Basic.NaturalIsomorphism
 > import Product.ProductCategory
 > import Limits.TerminalObject
 >
@@ -58,7 +61,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >     -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
 >     -> challenger h = challenger (exists x f g)
 >
-> productMorphism :
+> productMorphism : 
 >      (cat : Category)
 >   -> (a1, a2, b1, b2 : obj cat)
 >   -> (f : mor cat a1 a2)
@@ -151,5 +154,126 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >               (pComp (x,b) (y,b) (z,b) (MkProductMorphism f (identity cat b)) (MkProductMorphism g (identity cat b)))
 >
 > parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
->   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
->   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
+>   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (Carrier terminal)) a
+>   rightUnitorComponent a = Product.pi1 $ products a (Carrier terminal)
+>
+>   rightUnitorComm :
+>        (a, b : obj cat)
+>     -> (f : mor cat a b) -> compose cat _ _ _ (rightUnitorComponent a) f
+>      = compose cat _ _ _ (mapMor (bifunctorLeft cat (productFunctor cat products) (Carrier terminal)) a b f)
+>                          (rightUnitorComponent b)
+>   rightUnitorComm a b f = 
+>     rewrite rightIdentity cat (carrier (products a (Carrier terminal))) (Carrier terminal) (pi2 (products a (Carrier terminal))) in
+>     sym $ commutativityLeft (exists (products b (Carrier terminal))
+>                             (carrier (products a (Carrier terminal)))
+>                             (compose cat (carrier (products a (Carrier terminal))) a b (pi1 (products a (Carrier terminal))) f)
+>                             (pi2 (products a (Carrier terminal))))
+>
+>   rightUnitorNatTrans : NaturalTransformation cat cat (bifunctorLeft cat (productFunctor cat products) (Carrier terminal))
+>                                                       (idFunctor cat)
+>   rightUnitorNatTrans = MkNaturalTransformation rightUnitorComponent rightUnitorComm
+>
+>   rightUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products a (Carrier terminal))
+>   rightUnitorInverse a = challenger $ Product.exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a)
+>
+>   commutativeIdentity : (a, b : obj cat) -> let pab = products a b in 
+>                         CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
+>   commutativeIdentity a b = 
+>     MkCommutingMorphism (identity cat $ carrier $ products a b) 
+>                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b)) 
+>                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b)) 
+>
+>   productPi12Identity : (a, b : obj cat) -> let pab = products a b in 
+>                                            challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
+>   productPi12Identity a b = sym $ unique (products a b) (carrier $ products a b) (pi1 $ products a b) (pi2 $ products a b) (commutativeIdentity a b) 
+>
+
+potentialIdentity ; pi2 = pi1; pi2 = pi1 ; unique = unique
+potentialIdentity ; pi1 = pi1; p = pi1 ; unique = unique
+
+   commutingMorphismUniqueness : challenger (CommutingMorphism cat x a b (carrier pab) (pi1 pab) (pi2 pab) f g) = challenger (CommutingMorphism cat x a b (carrier pab) (pi1 pab) (pi2 pab) f g)
+
+
+>   potentialIdentity : (a : obj cat) -> mor cat (carrier $ products a (Carrier terminal)) (carrier $ products a (Carrier terminal))
+>   potentialIdentity a = compose cat
+>               (carrier (products a (Carrier terminal)))
+>               a
+>               (carrier (products a (Carrier terminal)))
+>               (pi1 (products a (Carrier terminal)))
+>               (challenger (exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a)))
+>
+>   potentialIdentityCommutingMorphism : (a : obj cat) -> let pa1 = products a (Carrier terminal) in  
+>                                                            CommutingMorphism cat (carrier pa1) a (Carrier terminal) (carrier pa1) (pi1 pa1) (pi2 pa1) (compose cat _ _ _ (potentialIdentity a) (pi1 pa1)) (compose cat _ _ _ (potentialIdentity a) (pi2 pa1))
+>   potentialIdentityCommutingMorphism a = ?wat1
+
+>
+>   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
+>   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a) 
+>     ?wat0
+>     (commutativityLeft $ Product.exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a))
+>
+>   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat products) (Carrier terminal))
+>                                                  (idFunctor cat)
+>   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
+
+rightUnitorInverse a ; 
+pi1 ; <id_A, unique> = id_(A x (Carrier terminal))
+
+A x 1 - pi1 -> A
+A x 1 - pi2 -> 1
+
+<pi1, pi2> = id_(A x 1)
+
+A x 1 - unique -> 1
+==> unique = pi2
+
+
+
+A x 1 -- pi1 --> A -- <id_A, unique> --> A x 1
+pi1;<id_A, unique>;pi2 = pi1 ; id_A = pi1
+pi1;<id_A, unique>;pi2 = pi1;unique = unique = pi2
+
+
+A x 1 -- pi2 --> 1
+  |              ^
+  |              |
+ pi1            pi2
+  |              |
+ \ /             |
+  A <-- pi1 -- A x 1
+
+
+
+exists a -> (id_a:a->a) -> (unique: a -> 1)
+rightUnitorComponent: A x 1 -- pi1 -> A 
+inverse: A --> A x (Carrier terminal)
+A -- inverse := <id_A, unique> --> A x Carrier terminal -- pi1 --> A
+
+
+
+A -- unique --> Carrier terminal
+A -- id --> A  
+
+
+A x 1 -- pi1 --> A
+    |                     |
+    |                     |
+  fxid1                f
+    |                     |
+   \ /                   \ / 
+B x 1 -- pi1 --> B
+
+
+
+
+pi2, ! 
+
+
+f: A --> B
+
+A x 1 -- f x id1 -> B x 1
+
+
+<pi1;f, pi2;id1> = <pi1;f,pi2;>
+
+<pi1;f,pi2;> ; pi1 = pi1;f
\ No newline at end of file
diff --git a/src/Limits/TerminalObject.lidr b/src/Limits/TerminalObject.lidr
index 1d5f28f..0b4f3c7 100644
--- a/src/Limits/TerminalObject.lidr
+++ b/src/Limits/TerminalObject.lidr
@@ -29,22 +29,22 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > record TerminalObject (cat : Category) where
 >   constructor MkTerminalObject
->   carrier : obj cat
->   exists  : (a : obj cat) -> mor cat a carrier
->   unique  : (a : obj cat) -> (f, g : mor cat a carrier) -> f = g
+>   Carrier : obj cat
+>   exists  : (a : obj cat) -> mor cat a Carrier
+>   unique  : (a : obj cat) -> (f, g : mor cat a Carrier) -> f = g
 >
 > composeTerminalMorphisms :
 >      (cat : Category)
 >   -> (a, b : TerminalObject cat)
->   -> mor cat (carrier a) (carrier a)
+>   -> mor cat (Carrier a) (Carrier a)
 > composeTerminalMorphisms cat a b =
->   compose cat (carrier a) (carrier b) (carrier a) (exists b (carrier a)) (exists a (carrier b))
+>   compose cat (Carrier a) (Carrier b) (Carrier a) (exists b (Carrier a)) (exists a (Carrier b))
 >
 > terminalObjectsAreIsomorphic :
 >      (cat : Category)
 >   -> (a, b : TerminalObject cat)
->   -> Isomorphism cat (carrier a) (carrier b) (exists b (carrier a))
+>   -> Isomorphism cat (Carrier a) (Carrier b) (exists b (Carrier a))
 > terminalObjectsAreIsomorphic cat a b = MkIsomorphism
->   (exists a (carrier b))
->   (unique a (carrier a) (composeTerminalMorphisms cat a b) (identity cat (carrier a)))
->   (unique b (carrier b) (composeTerminalMorphisms cat b a) (identity cat (carrier b)))
+>   (exists a (Carrier b))
+>   (unique a (Carrier a) (composeTerminalMorphisms cat a b) (identity cat (Carrier a)))
+>   (unique b (Carrier b) (composeTerminalMorphisms cat b a) (identity cat (Carrier b)))

From 55459cb4897b44ba57a2ea0e68970c076ac56ae6 Mon Sep 17 00:00:00 2001
From: Marco Perone <pasafama@gmail.com>
Date: Thu, 27 Jun 2019 09:13:17 +0200
Subject: [PATCH 08/13] fix style

---
 src/Limits/Product.lidr        | 126 +++++++++++++++++++--------------
 src/Limits/TerminalObject.lidr |  18 ++---
 2 files changed, 83 insertions(+), 61 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 619276b..899b940 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -61,7 +61,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >     -> (h : CommutingMorphism cat x a b carrier pi1 pi2 f g)
 >     -> challenger h = challenger (exists x f g)
 >
-> productMorphism : 
+> productMorphism :
 >      (cat : Category)
 >   -> (a1, a2, b1, b2 : obj cat)
 >   -> (f : mor cat a1 a2)
@@ -154,70 +154,92 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >               (pComp (x,b) (y,b) (z,b) (MkProductMorphism f (identity cat b)) (MkProductMorphism g (identity cat b)))
 >
 > parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
->   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (Carrier terminal)) a
->   rightUnitorComponent a = Product.pi1 $ products a (Carrier terminal)
+>   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
+>   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
 >
 >   rightUnitorComm :
 >        (a, b : obj cat)
->     -> (f : mor cat a b) -> compose cat _ _ _ (rightUnitorComponent a) f
->      = compose cat _ _ _ (mapMor (bifunctorLeft cat (productFunctor cat products) (Carrier terminal)) a b f)
+>     -> (f : mor cat a b)
+>     -> compose cat _ _ _ (rightUnitorComponent a) f
+>      = compose cat _ _ _ (mapMor (bifunctorLeft cat (productFunctor cat products) (carrier terminal)) a b f)
 >                          (rightUnitorComponent b)
->   rightUnitorComm a b f = 
->     rewrite rightIdentity cat (carrier (products a (Carrier terminal))) (Carrier terminal) (pi2 (products a (Carrier terminal))) in
->     sym $ commutativityLeft (exists (products b (Carrier terminal))
->                             (carrier (products a (Carrier terminal)))
->                             (compose cat (carrier (products a (Carrier terminal))) a b (pi1 (products a (Carrier terminal))) f)
->                             (pi2 (products a (Carrier terminal))))
+>   rightUnitorComm a b f =
+>     rewrite
+>       rightIdentity cat (carrier (products a (carrier terminal)))
+>                         (carrier terminal)
+>                         (pi2 (products a (carrier terminal)))
+>     in
+>       sym $ commutativityLeft (exists (products b (carrier terminal))
+>                               (carrier (products a (carrier terminal)))
+>                               (compose cat (carrier (products a (carrier terminal)))
+>                                            a b
+>                                            (pi1 (products a (carrier terminal)))
+>                                            f)
+>                               (pi2 (products a (carrier terminal))))
 >
->   rightUnitorNatTrans : NaturalTransformation cat cat (bifunctorLeft cat (productFunctor cat products) (Carrier terminal))
->                                                       (idFunctor cat)
+>   rightUnitorNatTrans : NaturalTransformation cat cat
+>                                               (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
+>                                               (idFunctor cat)
 >   rightUnitorNatTrans = MkNaturalTransformation rightUnitorComponent rightUnitorComm
 >
->   rightUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products a (Carrier terminal))
->   rightUnitorInverse a = challenger $ Product.exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a)
+>   rightUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products a (carrier terminal))
+>   rightUnitorInverse a = challenger $ Product.exists (products a (carrier terminal))
+>                                                      a
+>                                                      (identity cat a)
+>                                                      (exists terminal a)
 >
->   commutativeIdentity : (a, b : obj cat) -> let pab = products a b in 
->                         CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
->   commutativeIdentity a b = 
->     MkCommutingMorphism (identity cat $ carrier $ products a b) 
->                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b)) 
->                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b)) 
+>   commutativeIdentity :
+>        (a, b : obj cat)
+>     -> let pab = products a b in
+>        CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
+>   commutativeIdentity a b =
+>     MkCommutingMorphism (identity cat $ carrier $ products a b)
+>                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b))
+>                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b))
 >
->   productPi12Identity : (a, b : obj cat) -> let pab = products a b in 
->                                            challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
->   productPi12Identity a b = sym $ unique (products a b) (carrier $ products a b) (pi1 $ products a b) (pi2 $ products a b) (commutativeIdentity a b) 
+>   productPi12Identity :
+>        (a, b : obj cat)
+>     -> let pab = products a b in
+>        challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
+>   productPi12Identity a b = sym $ unique (products a b)
+>                                          (carrier $ products a b)
+>                                          (pi1 $ products a b)
+>                                          (pi2 $ products a b)
+>                                          (commutativeIdentity a b)
 >
-
-potentialIdentity ; pi2 = pi1; pi2 = pi1 ; unique = unique
-potentialIdentity ; pi1 = pi1; p = pi1 ; unique = unique
-
-   commutingMorphismUniqueness : challenger (CommutingMorphism cat x a b (carrier pab) (pi1 pab) (pi2 pab) f g) = challenger (CommutingMorphism cat x a b (carrier pab) (pi1 pab) (pi2 pab) f g)
-
-
->   potentialIdentity : (a : obj cat) -> mor cat (carrier $ products a (Carrier terminal)) (carrier $ products a (Carrier terminal))
+>   potentialIdentity :
+>        (a : obj cat)
+>     -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
 >   potentialIdentity a = compose cat
->               (carrier (products a (Carrier terminal)))
+>               (carrier (products a (carrier terminal)))
 >               a
->               (carrier (products a (Carrier terminal)))
->               (pi1 (products a (Carrier terminal)))
->               (challenger (exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a)))
+>               (carrier (products a (carrier terminal)))
+>               (pi1 (products a (carrier terminal)))
+>               (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
 >
->   potentialIdentityCommutingMorphism : (a : obj cat) -> let pa1 = products a (Carrier terminal) in  
->                                                            CommutingMorphism cat (carrier pa1) a (Carrier terminal) (carrier pa1) (pi1 pa1) (pi2 pa1) (compose cat _ _ _ (potentialIdentity a) (pi1 pa1)) (compose cat _ _ _ (potentialIdentity a) (pi2 pa1))
+>   potentialIdentityCommutingMorphism :
+>        (a : obj cat)
+>     -> let pa1 = products a (carrier terminal) in
+>        CommutingMorphism cat (carrier pa1)
+>                              a
+>                              (carrier terminal)
+>                              (carrier pa1)
+>                              (pi1 pa1) (pi2 pa1)
+>                              (compose cat _ _ _ (potentialIdentity a) (pi1 pa1))
+>                              (compose cat _ _ _ (potentialIdentity a) (pi2 pa1))
 >   potentialIdentityCommutingMorphism a = ?wat1
-
 >
 >   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
->   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a) 
+>   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a)
 >     ?wat0
->     (commutativityLeft $ Product.exists (products a (Carrier terminal)) a (identity cat a) (exists terminal a))
+>     (commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
 >
->   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat products) (Carrier terminal))
+>   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
 >                                                  (idFunctor cat)
 >   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
 
-rightUnitorInverse a ; 
-pi1 ; <id_A, unique> = id_(A x (Carrier terminal))
+rightUnitorInverse a ;
+pi1 ; <id_A, unique> = id_(A x (carrier terminal))
 
 A x 1 - pi1 -> A
 A x 1 - pi2 -> 1
@@ -245,14 +267,14 @@ A x 1 -- pi2 --> 1
 
 
 exists a -> (id_a:a->a) -> (unique: a -> 1)
-rightUnitorComponent: A x 1 -- pi1 -> A 
-inverse: A --> A x (Carrier terminal)
-A -- inverse := <id_A, unique> --> A x Carrier terminal -- pi1 --> A
+rightUnitorComponent: A x 1 -- pi1 -> A
+inverse: A --> A x (carrier terminal)
+A -- inverse := <id_A, unique> --> A x carrier terminal -- pi1 --> A
 
 
 
-A -- unique --> Carrier terminal
-A -- id --> A  
+A -- unique --> carrier terminal
+A -- id --> A
 
 
 A x 1 -- pi1 --> A
@@ -260,13 +282,13 @@ A x 1 -- pi1 --> A
     |                     |
   fxid1                f
     |                     |
-   \ /                   \ / 
+   \ /                   \ /
 B x 1 -- pi1 --> B
 
 
 
 
-pi2, ! 
+pi2, !
 
 
 f: A --> B
@@ -276,4 +298,4 @@ A x 1 -- f x id1 -> B x 1
 
 <pi1;f, pi2;id1> = <pi1;f,pi2;>
 
-<pi1;f,pi2;> ; pi1 = pi1;f
\ No newline at end of file
+<pi1;f,pi2;> ; pi1 = pi1;f
diff --git a/src/Limits/TerminalObject.lidr b/src/Limits/TerminalObject.lidr
index 0b4f3c7..1d5f28f 100644
--- a/src/Limits/TerminalObject.lidr
+++ b/src/Limits/TerminalObject.lidr
@@ -29,22 +29,22 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > record TerminalObject (cat : Category) where
 >   constructor MkTerminalObject
->   Carrier : obj cat
->   exists  : (a : obj cat) -> mor cat a Carrier
->   unique  : (a : obj cat) -> (f, g : mor cat a Carrier) -> f = g
+>   carrier : obj cat
+>   exists  : (a : obj cat) -> mor cat a carrier
+>   unique  : (a : obj cat) -> (f, g : mor cat a carrier) -> f = g
 >
 > composeTerminalMorphisms :
 >      (cat : Category)
 >   -> (a, b : TerminalObject cat)
->   -> mor cat (Carrier a) (Carrier a)
+>   -> mor cat (carrier a) (carrier a)
 > composeTerminalMorphisms cat a b =
->   compose cat (Carrier a) (Carrier b) (Carrier a) (exists b (Carrier a)) (exists a (Carrier b))
+>   compose cat (carrier a) (carrier b) (carrier a) (exists b (carrier a)) (exists a (carrier b))
 >
 > terminalObjectsAreIsomorphic :
 >      (cat : Category)
 >   -> (a, b : TerminalObject cat)
->   -> Isomorphism cat (Carrier a) (Carrier b) (exists b (Carrier a))
+>   -> Isomorphism cat (carrier a) (carrier b) (exists b (carrier a))
 > terminalObjectsAreIsomorphic cat a b = MkIsomorphism
->   (exists a (Carrier b))
->   (unique a (Carrier a) (composeTerminalMorphisms cat a b) (identity cat (Carrier a)))
->   (unique b (Carrier b) (composeTerminalMorphisms cat b a) (identity cat (Carrier b)))
+>   (exists a (carrier b))
+>   (unique a (carrier a) (composeTerminalMorphisms cat a b) (identity cat (carrier a)))
+>   (unique b (carrier b) (composeTerminalMorphisms cat b a) (identity cat (carrier b)))

From c124b7d6642f3f80fa40684c1b7d537e19e41a5f Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Thu, 11 Jul 2019 18:26:21 +0300
Subject: [PATCH 09/13] live session 11.07.2019

---
 src/Limits/Product.lidr        | 122 +++++++++++++--------------------
 src/Limits/TerminalObject.lidr |   1 +
 2 files changed, 49 insertions(+), 74 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 899b940..3ae9100 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -217,85 +217,59 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >               (pi1 (products a (carrier terminal)))
 >               (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
 >
->   potentialIdentityCommutingMorphism :
->        (a : obj cat)
->     -> let pa1 = products a (carrier terminal) in
->        CommutingMorphism cat (carrier pa1)
->                              a
->                              (carrier terminal)
->                              (carrier pa1)
->                              (pi1 pa1) (pi2 pa1)
->                              (compose cat _ _ _ (potentialIdentity a) (pi1 pa1))
->                              (compose cat _ _ _ (potentialIdentity a) (pi2 pa1))
->   potentialIdentityCommutingMorphism a = ?wat1
->
 >   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
 >   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a)
->     ?wat0
+>     (rewrite sym $ productPi12Identity a (carrier terminal) in 
+>      Product.unique 
+>             (products a (carrier terminal))
+>             (carrier $ products a (carrier terminal)) 
+>             (pi1 (products a (carrier terminal))) 
+>             (pi2 (products a (carrier terminal)))
+>             (MkCommutingMorphism 
+>                (compose cat
+>                        (carrier (products a (carrier terminal)))
+>                         a
+>                        (carrier (products a (carrier terminal)))
+>                        (pi1 (products a (carrier terminal)))
+>                        (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                ) 
+>                (rewrite sym $ associativity cat (carrier (products a (carrier terminal)))
+>                                                  a
+>                                                 (carrier (products a (carrier terminal))) 
+>                                                  a 
+>                                                 (pi1 (products a (carrier terminal)))
+>                                                 (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                                                 (pi1 (products a (carrier terminal))) in
+>                 rewrite commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a) in
+>                 rightIdentity cat (carrier (products a (carrier terminal))) a (pi1 (products a (carrier terminal)))
+>                ) 
+>                (TerminalObject.unique terminal (carrier (products a (carrier terminal))) 
+>                   (compose cat
+>                           (carrier (products a (carrier terminal)))
+>                           (carrier (products a (carrier terminal)))
+>                           (carrier terminal)
+>                           (compose cat
+>                                    (carrier (products a (carrier terminal)))
+>                                    a
+>                                    (carrier (products a (carrier terminal)))
+>                                    (pi1 (products a (carrier terminal)))
+>                                    (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))))
+>                           (pi2 (products a (carrier terminal))))
+>                  (pi2 (products a (carrier terminal)))
+>             )
+>           )
+>     )
 >     (commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
 >
 >   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
 >                                                  (idFunctor cat)
 >   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
+>
 
-rightUnitorInverse a ;
-pi1 ; <id_A, unique> = id_(A x (carrier terminal))
-
-A x 1 - pi1 -> A
-A x 1 - pi2 -> 1
-
-<pi1, pi2> = id_(A x 1)
-
-A x 1 - unique -> 1
-==> unique = pi2
-
-
-
-A x 1 -- pi1 --> A -- <id_A, unique> --> A x 1
-pi1;<id_A, unique>;pi2 = pi1 ; id_A = pi1
-pi1;<id_A, unique>;pi2 = pi1;unique = unique = pi2
-
-
-A x 1 -- pi2 --> 1
-  |              ^
-  |              |
- pi1            pi2
-  |              |
- \ /             |
-  A <-- pi1 -- A x 1
-
-
-
-exists a -> (id_a:a->a) -> (unique: a -> 1)
-rightUnitorComponent: A x 1 -- pi1 -> A
-inverse: A --> A x (carrier terminal)
-A -- inverse := <id_A, unique> --> A x carrier terminal -- pi1 --> A
-
-
-
-A -- unique --> carrier terminal
-A -- id --> A
-
-
-A x 1 -- pi1 --> A
-    |                     |
-    |                     |
-  fxid1                f
-    |                     |
-   \ /                   \ /
-B x 1 -- pi1 --> B
-
-
-
-
-pi2, !
-
-
-f: A --> B
-
-A x 1 -- f x id1 -> B x 1
-
-
-<pi1;f, pi2;id1> = <pi1;f,pi2;>
-
-<pi1;f,pi2;> ; pi1 = pi1;f
+* dualize for left unitor
+* Prove composition law for product (?compLaw hole)
+* Define associator components: (A x B) x C --> A x (B x C)
+* Prove they are isomorphisms (Horrible)
+* Prove they define a natural transformation
+* Prove Triangle identity
+* Prove Pentagon identity (Horrible too) 
\ No newline at end of file
diff --git a/src/Limits/TerminalObject.lidr b/src/Limits/TerminalObject.lidr
index 1d5f28f..69ea65b 100644
--- a/src/Limits/TerminalObject.lidr
+++ b/src/Limits/TerminalObject.lidr
@@ -26,6 +26,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > %access public export
 > %default total
+> %auto_implicits off
 >
 > record TerminalObject (cat : Category) where
 >   constructor MkTerminalObject

From ff8efe913bea4fcc7e67a1313e62999b1406e91c Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Sun, 21 Jul 2019 02:31:09 +0300
Subject: [PATCH 10/13] dualize for left unitor

---
 src/Limits/Product.lidr | 239 ++++++++++++++++++++++++++++++----------
 1 file changed, 181 insertions(+), 58 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 3ae9100..430281a 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -153,7 +153,65 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >               (leftIdentity cat b b (identity cat b))
 >               (pComp (x,b) (y,b) (z,b) (MkProductMorphism f (identity cat b)) (MkProductMorphism g (identity cat b)))
 >
+> bifunctorRight :
+>      (cat : Category)
+>   -> (fun : CFunctor (productCategory cat cat) cat)
+>   -> (a : obj cat)
+>   -> CFunctor cat cat
+> bifunctorRight cat (MkCFunctor mapObj mapMor pId pComp) a = MkCFunctor mapObj' mapMor' pId' pComp'
+>   where
+>     mapObj' : obj cat -> obj cat
+>     mapObj' x = mapObj (a, x)
+>
+>     mapMor' : (x, y : obj cat) -> mor cat x y -> mor cat (mapObj' x) (mapObj' y)
+>     mapMor' x y mor = mapMor (a, x) (a, y) (MkProductMorphism (identity cat a) mor)
+>
+>     pId' :
+>          (x : obj cat)
+>       -> mapMor (a, x) (a, x) (MkProductMorphism (identity cat a) (identity cat x))
+>        = identity cat (mapObj (a, x))
+>     pId' x = pId (a, x)
+>
+>     pComp' :
+>          (x, y, z : obj cat)
+>       -> (f : mor cat x y)
+>       -> (g : mor cat y z)
+>       -> mapMor (a, x) (a, z) (MkProductMorphism (identity cat a) (compose cat x y z f g))
+>        = compose cat (mapObj (a, x))
+>                      (mapObj (a, y))
+>                      (mapObj (a, z))
+>                      (mapMor (a, x) (a, y) (MkProductMorphism (identity cat a) f))
+>                      (mapMor (a, y) (a, z) (MkProductMorphism (identity cat a) g))
+>     pComp' x y z f g =
+>       replace {P=\q => mapMor (a, x) (a, z) (MkProductMorphism q (compose cat x y z f g))
+>                      = compose cat (mapObj (a, x))
+>                                    (mapObj (a, y))
+>                                    (mapObj (a, z))
+>                                    (mapMor (a, x) (a, y) (MkProductMorphism (identity cat a) f))
+>                                    (mapMor (a, y) (a, z) (MkProductMorphism (identity cat a) g))}
+>               (rightIdentity cat a a (identity cat a))
+>               (pComp (a,x) (a,y) (a,z) (MkProductMorphism (identity cat a) f) (MkProductMorphism (identity cat a) g))
+>
 > parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
+>   commutativeIdentity :
+>        (a, b : obj cat)
+>     -> let pab = products a b in
+>        CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
+>   commutativeIdentity a b =
+>     MkCommutingMorphism (identity cat $ carrier $ products a b)
+>                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b))
+>                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b))
+>
+>   productPi12Identity :
+>        (a, b : obj cat)
+>     -> let pab = products a b in
+>        challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
+>   productPi12Identity a b = sym $ unique (products a b)
+>                                          (carrier $ products a b)
+>                                          (pi1 $ products a b)
+>                                          (pi2 $ products a b)
+>                                          (commutativeIdentity a b)
+>
 >   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
 >   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
 >
@@ -165,17 +223,17 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                          (rightUnitorComponent b)
 >   rightUnitorComm a b f =
 >     rewrite
->       rightIdentity cat (carrier (products a (carrier terminal)))
+>       rightIdentity cat (carrier $ products a (carrier terminal))
 >                         (carrier terminal)
->                         (pi2 (products a (carrier terminal)))
+>                         (pi2 $ products a (carrier terminal))
 >     in
 >       sym $ commutativityLeft (exists (products b (carrier terminal))
->                               (carrier (products a (carrier terminal)))
->                               (compose cat (carrier (products a (carrier terminal)))
->                                            a b
->                                            (pi1 (products a (carrier terminal)))
->                                            f)
->                               (pi2 (products a (carrier terminal))))
+>                                       (carrier $ products a (carrier terminal))
+>                                       (compose cat (carrier $ products a (carrier terminal))
+>                                                    a b
+>                                                    (pi1 $ products a (carrier terminal))
+>                                                    f)
+>                                       (pi2 $ products a (carrier terminal)))
 >
 >   rightUnitorNatTrans : NaturalTransformation cat cat
 >                                               (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
@@ -188,34 +246,19 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                                      (identity cat a)
 >                                                      (exists terminal a)
 >
->   commutativeIdentity :
->        (a, b : obj cat)
->     -> let pab = products a b in
->        CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
->   commutativeIdentity a b =
->     MkCommutingMorphism (identity cat $ carrier $ products a b)
->                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b))
->                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b))
->
->   productPi12Identity :
->        (a, b : obj cat)
->     -> let pab = products a b in
->        challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
->   productPi12Identity a b = sym $ unique (products a b)
->                                          (carrier $ products a b)
->                                          (pi1 $ products a b)
->                                          (pi2 $ products a b)
->                                          (commutativeIdentity a b)
->
->   potentialIdentity :
->        (a : obj cat)
->     -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
->   potentialIdentity a = compose cat
->               (carrier (products a (carrier terminal)))
->               a
->               (carrier (products a (carrier terminal)))
->               (pi1 (products a (carrier terminal)))
->               (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+   
+   doesn't seem necessary
+  
+   potentialIdentity :
+        (a : obj cat)
+     -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
+   potentialIdentity a = compose cat
+               (carrier $ products a (carrier terminal))
+               a
+               (carrier $ products a (carrier terminal))
+               (pi1 $ products a (carrier terminal))
+               (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+
 >
 >   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
 >   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a)
@@ -223,40 +266,40 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >      Product.unique 
 >             (products a (carrier terminal))
 >             (carrier $ products a (carrier terminal)) 
->             (pi1 (products a (carrier terminal))) 
->             (pi2 (products a (carrier terminal)))
+>             (pi1 $ products a (carrier terminal)) 
+>             (pi2 $ products a (carrier terminal))
 >             (MkCommutingMorphism 
 >                (compose cat
->                        (carrier (products a (carrier terminal)))
+>                        (carrier $ products a (carrier terminal))
 >                         a
->                        (carrier (products a (carrier terminal)))
->                        (pi1 (products a (carrier terminal)))
->                        (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                        (carrier $ products a (carrier terminal))
+>                        (pi1 $ products a (carrier terminal))
+>                        (challenger $ exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
 >                ) 
->                (rewrite sym $ associativity cat (carrier (products a (carrier terminal)))
+>                (rewrite sym $ associativity cat (carrier $ products a (carrier terminal))
 >                                                  a
->                                                 (carrier (products a (carrier terminal))) 
+>                                                 (carrier $ products a (carrier terminal)) 
 >                                                  a 
->                                                 (pi1 (products a (carrier terminal)))
+>                                                 (pi1 $ products a (carrier terminal))
 >                                                 (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
->                                                 (pi1 (products a (carrier terminal))) in
+>                                                 (pi1 $ products a (carrier terminal)) in
 >                 rewrite commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a) in
->                 rightIdentity cat (carrier (products a (carrier terminal))) a (pi1 (products a (carrier terminal)))
+>                 rightIdentity cat (carrier $ products a (carrier terminal)) a (pi1 $ products a (carrier terminal))
 >                ) 
->                (TerminalObject.unique terminal (carrier (products a (carrier terminal))) 
+>                (TerminalObject.unique terminal (carrier $ products a (carrier terminal)) 
 >                   (compose cat
->                           (carrier (products a (carrier terminal)))
->                           (carrier (products a (carrier terminal)))
+>                           (carrier $ products a (carrier terminal))
+>                           (carrier $ products a (carrier terminal))
 >                           (carrier terminal)
 >                           (compose cat
->                                    (carrier (products a (carrier terminal)))
+>                                    (carrier $ products a (carrier terminal))
 >                                    a
->                                    (carrier (products a (carrier terminal)))
->                                    (pi1 (products a (carrier terminal)))
->                                    (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))))
->                           (pi2 (products a (carrier terminal))))
->                  (pi2 (products a (carrier terminal)))
->             )
+>                                    (carrier $ products a (carrier terminal))
+>                                    (pi1 $ products a (carrier terminal))
+>                                    (challenger $ exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                           (pi2 $ products a (carrier terminal)))
+>                  (pi2 $ products a (carrier terminal))
+>                )
 >           )
 >     )
 >     (commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
@@ -265,8 +308,88 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                                  (idFunctor cat)
 >   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
 >
+>   leftUnitorComponent : (a : obj cat) -> mor cat (carrier $ products (carrier terminal) a) a
+>   leftUnitorComponent a = Product.pi2 $ products (carrier terminal) a
+>
+>   leftUnitorComm :
+>        (a, b : obj cat)
+>     -> (f : mor cat a b)
+>     -> compose cat _ _ _ (leftUnitorComponent a) f
+>      = compose cat _ _ _ (mapMor (bifunctorRight cat (productFunctor cat products) (carrier terminal)) a b f)
+>                          (leftUnitorComponent b)
+>   leftUnitorComm a b f = 
+>     rewrite
+>       rightIdentity cat (carrier $ products (carrier terminal) a)
+>                         (carrier terminal)
+>                         (pi1 $ products (carrier terminal) a)
+>      in
+>       sym $ commutativityRight (exists (products (carrier terminal) b)
+>                                        (carrier $ products (carrier terminal) a)
+>                                        (pi1 $ products (carrier terminal) a)
+>                                        (compose cat (carrier $ products (carrier terminal) a)
+>                                                     a b
+>                                                     (pi2 $ products (carrier terminal) a)
+>                                                     f))
+>
+>   leftUnitorNatTrans : NaturalTransformation cat cat
+>                                               (bifunctorRight cat (productFunctor cat products) (carrier terminal))
+>                                               (idFunctor cat)
+>   leftUnitorNatTrans = MkNaturalTransformation leftUnitorComponent leftUnitorComm
+>
+>   leftUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products (carrier terminal) a)
+>   leftUnitorInverse a = challenger $ Product.exists (products (carrier terminal) a)
+>                                                     a
+>                                                     (exists terminal a)
+>                                                     (identity cat a)
+>
+>   leftUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (leftUnitorComponent a)
+>   leftUnitorIsomorphism a = MkIsomorphism (leftUnitorInverse a) 
+>     (rewrite sym $ productPi12Identity (carrier terminal) a in 
+>      Product.unique 
+>             (products (carrier terminal) a)
+>             (carrier $ products (carrier terminal) a) 
+>             (pi1 $ products (carrier terminal) a) 
+>             (pi2 $ products (carrier terminal) a)
+>             (MkCommutingMorphism 
+>                (compose cat
+>                         (carrier $ products (carrier terminal) a)
+>                         a
+>                         (carrier $ products (carrier terminal) a)
+>                         (pi2 $ products (carrier terminal) a)
+>                         (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
+>                )
+>                (TerminalObject.unique terminal (carrier $ products (carrier terminal) a) 
+>                   (compose cat
+>                           (carrier $ products (carrier terminal) a)
+>                           (carrier $ products (carrier terminal) a)
+>                           (carrier terminal)
+>                           (compose cat
+>                                    (carrier $ products (carrier terminal) a)
+>                                    a
+>                                    (carrier $ products (carrier terminal) a)
+>                                    (pi2 $ products (carrier terminal) a)
+>                                    (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a)))
+>                           (pi1 $ products (carrier terminal) a))
+>                  (pi1 $ products (carrier terminal) a)
+>                )
+>                (rewrite sym $ associativity cat (carrier $ products (carrier terminal) a)
+>                                                  a
+>                                                 (carrier $ products (carrier terminal) a) 
+>                                                  a 
+>                                                 (pi2 $ products (carrier terminal) a)
+>                                                 (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
+>                                                 (pi2 $ products (carrier terminal) a) in
+>                 rewrite commutativityRight $ Product.exists (products (carrier terminal) a) a (exists terminal a) (identity cat a)  in
+>                 rightIdentity cat (carrier $ products (carrier terminal) a) a (pi2 $ products (carrier terminal) a)
+>                )
+>             )
+>     ) 
+>     (commutativityRight $ Product.exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
+>
+>   leftUnitorNatIso : NaturalIsomorphism cat cat (bifunctorRight cat (productFunctor cat products) (carrier terminal))
+>                                                 (idFunctor cat)
+>   leftUnitorNatIso = MkNaturalIsomorphism leftUnitorNatTrans leftUnitorIsomorphism
 
-* dualize for left unitor
 * Prove composition law for product (?compLaw hole)
 * Define associator components: (A x B) x C --> A x (B x C)
 * Prove they are isomorphisms (Horrible)

From aa93f17eeb55564ac80d8f96228cdcbe872f0bae Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Thu, 25 Jul 2019 01:18:04 +0300
Subject: [PATCH 11/13] prove compLaw

---
 src/Limits/Product.lidr | 85 ++++++++++++++++++++++++++++++++++-------
 1 file changed, 72 insertions(+), 13 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 430281a..3ef2556 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -79,7 +79,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >      (cat : Category)
 >   -> (productObj : catHasProducts cat)
 >   -> CFunctor (productCategory cat cat) cat
-> productFunctor cat productObj = MkCFunctor mapObj mapMor idLaw ?compLaw
+> productFunctor cat productObj = MkCFunctor mapObj mapMor idLaw compLaw
 >   where
 >     mapObj : (obj cat, obj cat) -> obj cat
 >     mapObj (a,b) = carrier $ productObj a b
@@ -110,6 +110,66 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
 >                                (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
 >                                (identityCommutingMorphism a b)
+>     compComMor : (a1,a2,b1,b2,c1,c2 : obj cat) 
+>               -> (f1 : mor cat a1 b1) -> (f2 : mor cat a2 b2) 
+>               -> (g1 : mor cat b1 c1) -> (g2 : mor cat b2 c2)
+>               -> CommutingMorphism cat (carrier (productObj a1 a2)) c1 c2 
+>                                    (carrier (productObj c1 c2)) (pi1 (productObj c1 c2)) (pi2 (productObj c1 c2)) 
+>                                    (compose cat (carrier (productObj a1 a2)) a1 c1 (pi1 (productObj a1 a2)) (compose cat a1 b1 c1 f1 g1))
+>                                    (compose cat (carrier (productObj a1 a2)) a2 c2 (pi2 (productObj a1 a2)) (compose cat a2 b2 c2 f2 g2))
+>     compComMor a1 a2 b1 b2 c1 c2 f1 f2 g1 g2 = 
+>       let 
+>         cmab = exists (productObj b1 b2)
+>                       (carrier (productObj a1 a2))
+>                       (compose cat (carrier (productObj a1 a2)) a1 b1 (pi1 (productObj a1 a2)) f1)
+>                       (compose cat (carrier (productObj a1 a2)) a2 b2 (pi2 (productObj a1 a2)) f2)
+>         cmbc = exists (productObj c1 c2)
+>                       (carrier (productObj b1 b2))
+>                       (compose cat (carrier (productObj b1 b2)) b1 c1 (pi1 (productObj b1 b2)) g1)
+>                       (compose cat (carrier (productObj b1 b2)) b2 c2 (pi2 (productObj b1 b2)) g2)
+>        in
+>       MkCommutingMorphism (compose cat
+>                                    (carrier (productObj a1 a2))
+>                                    (carrier (productObj b1 b2))
+>                                    (carrier (productObj c1 c2))
+>                                    (challenger cmab)
+>                                    (challenger cmbc)) 
+>                           (rewrite sym $ associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) (carrier (productObj c1 c2)) c1
+>                                                            (challenger cmab)
+>                                                            (challenger cmbc)
+>                                                            (pi1 (productObj c1 c2)) in
+>                            rewrite commutativityLeft cmbc in 
+>                            rewrite associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) b1 c1
+>                                                      (challenger cmab)
+>                                                      (pi1 (productObj b1 b2)) 
+>                                                      g1 in
+>                            rewrite commutativityLeft cmab in 
+>                            sym $ associativity cat (carrier (productObj a1 a2)) a1 b1 c1 
+>                                                    (pi1 (productObj a1 a2)) f1 g1) 
+>                           (rewrite sym $ associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) (carrier (productObj c1 c2)) c2
+>                                                            (challenger cmab)
+>                                                            (challenger cmbc)
+>                                                            (pi2 (productObj c1 c2)) in
+>                            rewrite commutativityRight cmbc in 
+>                            rewrite associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) b2 c2
+>                                                      (challenger cmab)
+>                                                      (pi2 (productObj b1 b2)) 
+>                                                      g2 in
+>                            rewrite commutativityRight cmab in 
+>                            sym $ associativity cat (carrier (productObj a1 a2)) a2 b2 c2 
+>                                                    (pi2 (productObj a1 a2)) f2 g2) 
+>     compLaw : 
+>          (a,b,c : (obj cat, obj cat)) ->
+>          (f : ProductMorphism cat cat a b) ->
+>          (g : ProductMorphism cat cat b c) ->
+>          mapMor a c (productCompose a b c f g) =
+>          compose cat (mapObj a) (mapObj b) (mapObj c) (mapMor a b f) (mapMor b c g)
+>     compLaw (a1,a2) (b1,b2) (c1,c2) (MkProductMorphism f1 f2) (MkProductMorphism g1 g2) = 
+>       sym $ unique (productObj c1 c2) 
+>                    (carrier (productObj a1 a2)) 
+>                    (compose cat (carrier (productObj a1 a2)) a1 c1 (pi1 (productObj a1 a2)) (compose cat a1 b1 c1 f1 g1))
+>                    (compose cat (carrier (productObj a1 a2)) a2 c2 (pi2 (productObj a1 a2)) (compose cat a2 b2 c2 f2 g2))
+>                    (compComMor a1 a2 b1 b2 c1 c2 f1 f2 g1 g2)
 >
 > catHasTerminalObj : Category -> Type
 > catHasTerminalObj = TerminalObject
@@ -246,18 +306,18 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                                      (identity cat a)
 >                                                      (exists terminal a)
 >
-   
-   doesn't seem necessary
   
-   potentialIdentity :
-        (a : obj cat)
-     -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
-   potentialIdentity a = compose cat
-               (carrier $ products a (carrier terminal))
-               a
-               (carrier $ products a (carrier terminal))
-               (pi1 $ products a (carrier terminal))
-               (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
+  doesn't seem necessary
+ 
+  potentialIdentity :
+       (a : obj cat)
+    -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
+  potentialIdentity a = compose cat
+              (carrier $ products a (carrier terminal))
+              a
+              (carrier $ products a (carrier terminal))
+              (pi1 $ products a (carrier terminal))
+              (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
 
 >
 >   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
@@ -390,7 +450,6 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                                 (idFunctor cat)
 >   leftUnitorNatIso = MkNaturalIsomorphism leftUnitorNatTrans leftUnitorIsomorphism
 
-* Prove composition law for product (?compLaw hole)
 * Define associator components: (A x B) x C --> A x (B x C)
 * Prove they are isomorphisms (Horrible)
 * Prove they define a natural transformation

From 2c832990496a4b20d7e9afa524f4aa734b00893e Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Thu, 25 Jul 2019 01:27:17 +0300
Subject: [PATCH 12/13] prettify compLaw

---
 src/Limits/Product.lidr | 54 +++++++++++++++--------------------------
 1 file changed, 20 insertions(+), 34 deletions(-)

diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 3ef2556..151a1be 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -119,45 +119,31 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                    (compose cat (carrier (productObj a1 a2)) a2 c2 (pi2 (productObj a1 a2)) (compose cat a2 b2 c2 f2 g2))
 >     compComMor a1 a2 b1 b2 c1 c2 f1 f2 g1 g2 = 
 >       let 
->         cmab = exists (productObj b1 b2)
->                       (carrier (productObj a1 a2))
->                       (compose cat (carrier (productObj a1 a2)) a1 b1 (pi1 (productObj a1 a2)) f1)
->                       (compose cat (carrier (productObj a1 a2)) a2 b2 (pi2 (productObj a1 a2)) f2)
->         cmbc = exists (productObj c1 c2)
->                       (carrier (productObj b1 b2))
->                       (compose cat (carrier (productObj b1 b2)) b1 c1 (pi1 (productObj b1 b2)) g1)
->                       (compose cat (carrier (productObj b1 b2)) b2 c2 (pi2 (productObj b1 b2)) g2)
+>         pa = productObj a1 a2
+>         pb = productObj b1 b2
+>         pc = productObj c1 c2
+>         cmab = exists pb (carrier pa) (compose cat (carrier pa) a1 b1 (pi1 pa) f1)
+>                                       (compose cat (carrier pa) a2 b2 (pi2 pa) f2)
+>         cmbc = exists pc (carrier pb) (compose cat (carrier pb) b1 c1 (pi1 pb) g1)
+>                                       (compose cat (carrier pb) b2 c2 (pi2 pb) g2)
 >        in
->       MkCommutingMorphism (compose cat
->                                    (carrier (productObj a1 a2))
->                                    (carrier (productObj b1 b2))
->                                    (carrier (productObj c1 c2))
->                                    (challenger cmab)
->                                    (challenger cmbc)) 
->                           (rewrite sym $ associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) (carrier (productObj c1 c2)) c1
->                                                            (challenger cmab)
->                                                            (challenger cmbc)
->                                                            (pi1 (productObj c1 c2)) in
+>       MkCommutingMorphism (compose cat (carrier pa) (carrier pb) (carrier pc) (challenger cmab) (challenger cmbc)) 
+>                           (rewrite sym $ associativity cat (carrier pa) (carrier pb) (carrier pc) c1
+>                                                            (challenger cmab) (challenger cmbc) (pi1 pc) in
 >                            rewrite commutativityLeft cmbc in 
->                            rewrite associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) b1 c1
->                                                      (challenger cmab)
->                                                      (pi1 (productObj b1 b2)) 
->                                                      g1 in
+>                            rewrite associativity cat (carrier pa) (carrier pb) b1 c1
+>                                                      (challenger cmab) (pi1 pb) g1 in
 >                            rewrite commutativityLeft cmab in 
->                            sym $ associativity cat (carrier (productObj a1 a2)) a1 b1 c1 
->                                                    (pi1 (productObj a1 a2)) f1 g1) 
->                           (rewrite sym $ associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) (carrier (productObj c1 c2)) c2
->                                                            (challenger cmab)
->                                                            (challenger cmbc)
->                                                            (pi2 (productObj c1 c2)) in
+>                            sym $ associativity cat (carrier pa) a1 b1 c1 
+>                                                    (pi1 pa) f1 g1) 
+>                           (rewrite sym $ associativity cat (carrier pa) (carrier pb) (carrier pc) c2
+>                                                            (challenger cmab) (challenger cmbc) (pi2 pc) in
 >                            rewrite commutativityRight cmbc in 
->                            rewrite associativity cat (carrier (productObj a1 a2)) (carrier (productObj b1 b2)) b2 c2
->                                                      (challenger cmab)
->                                                      (pi2 (productObj b1 b2)) 
->                                                      g2 in
+>                            rewrite associativity cat (carrier pa) (carrier pb) b2 c2
+>                                                      (challenger cmab) (pi2 pb) g2 in
 >                            rewrite commutativityRight cmab in 
->                            sym $ associativity cat (carrier (productObj a1 a2)) a2 b2 c2 
->                                                    (pi2 (productObj a1 a2)) f2 g2) 
+>                            sym $ associativity cat (carrier pa) a2 b2 c2 
+>                                                    (pi2 pa) f2 g2) 
 >     compLaw : 
 >          (a,b,c : (obj cat, obj cat)) ->
 >          (f : ProductMorphism cat cat a b) ->

From f60b6e29b4573fa9f3fbe0311c42ba2641190993 Mon Sep 17 00:00:00 2001
From: Alex Gryzlov <skyrodent@gmail.com>
Date: Thu, 25 Jul 2019 18:32:50 +0300
Subject: [PATCH 13/13] live session 25.07.2019

---
 idris-ct.ipkg                   |   3 +
 src/Limits/MonoidalProduct.lidr | 268 ++++++++++++++++++++++++++++++++
 src/Limits/Product.lidr         | 268 ++++----------------------------
 3 files changed, 300 insertions(+), 239 deletions(-)
 create mode 100644 src/Limits/MonoidalProduct.lidr

diff --git a/idris-ct.ipkg b/idris-ct.ipkg
index 2214523..6e9caf2 100644
--- a/idris-ct.ipkg
+++ b/idris-ct.ipkg
@@ -35,6 +35,9 @@ modules =
   Idris.FunctorAsCFunctor,
   Idris.TypesAsCategory,
   Idris.TypesAsCategoryExtensional,
+  Limits.TerminalObject,
+  Limits.Product,
+  Limits.MonoidalProduct,
   Monoid.Monoid,
   Monoid.MonoidAsCategory,
   Monoid.MonoidMorphism,
diff --git a/src/Limits/MonoidalProduct.lidr b/src/Limits/MonoidalProduct.lidr
new file mode 100644
index 0000000..ec2dd3b
--- /dev/null
+++ b/src/Limits/MonoidalProduct.lidr
@@ -0,0 +1,268 @@
+\iffalse
+SPDX-License-Identifier: AGPL-3.0-only
+
+This file is part of `idris-ct` Category Theory in Idris library.
+
+Copyright (C) 2019 Stichting Statebox <https://statebox.nl>
+
+This program is free software: you can redistribute it and/or modify
+it under the terms of the GNU Affero General Public License as published by
+the Free Software Foundation, either version 3 of the License, or
+(at your option) any later version.
+
+This program is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+GNU Affero General Public License for more details.
+
+You should have received a copy of the GNU Affero General Public License
+along with this program.  If not, see <https://www.gnu.org/licenses/>.
+\fi
+
+> module Limits.MonoidalProduct
+>
+> import Basic.Category
+> import Basic.Functor
+> import Basic.Isomorphism
+> import Basic.NaturalTransformation
+> import Basic.NaturalIsomorphism
+> import Product.ProductCategory
+> import Limits.TerminalObject
+> import Limits.Product
+>
+> %access public export
+> %default total
+> %auto_implicits off
+>
+> parameters (cat : Category, product : catHasProducts cat, terminal : TerminalObject cat)
+>   commutativeIdentity :
+>        (a, b : obj cat)
+>     -> let pab = product a b in
+>        CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
+>   commutativeIdentity a b =
+>     MkCommutingMorphism (identity cat $ carrier $ product a b)
+>                         (leftIdentity cat (carrier $ product a b) a (pi1 $ product a b))
+>                         (leftIdentity cat (carrier $ product a b) b (pi2 $ product a b))
+>
+>   productPi12Identity :
+>        (a, b : obj cat)
+>     -> let pab = product a b in
+>        challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
+>   productPi12Identity a b = sym $ unique (product a b)
+>                                          (carrier $ product a b)
+>                                          (pi1 $ product a b)
+>                                          (pi2 $ product a b)
+>                                          (commutativeIdentity a b)
+>
+>   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ product a (carrier terminal)) a
+>   rightUnitorComponent a = Product.pi1 $ product a (carrier terminal)
+>
+>   rightUnitorComm :
+>        (a, b : obj cat)
+>     -> (f : mor cat a b)
+>     -> compose cat _ _ _ (rightUnitorComponent a) f
+>      = compose cat _ _ _ (mapMor (bifunctorLeft cat (productFunctor cat product) (carrier terminal)) a b f)
+>                          (rightUnitorComponent b)
+>   rightUnitorComm a b f =
+>     rewrite
+>       rightIdentity cat (carrier $ product a (carrier terminal))
+>                         (carrier terminal)
+>                         (pi2 $ product a (carrier terminal))
+>     in
+>       sym $ commutativityLeft (exists (product b (carrier terminal))
+>                                       (carrier $ product a (carrier terminal))
+>                                       (compose cat (carrier $ product a (carrier terminal))
+>                                                    a b
+>                                                    (pi1 $ product a (carrier terminal))
+>                                                    f)
+>                                       (pi2 $ product a (carrier terminal)))
+>
+>   rightUnitorNatTrans : NaturalTransformation cat cat
+>                                               (bifunctorLeft cat (productFunctor cat product) (carrier terminal))
+>                                               (idFunctor cat)
+>   rightUnitorNatTrans = MkNaturalTransformation rightUnitorComponent rightUnitorComm
+>
+>   rightUnitorInverse : (a : obj cat) -> mor cat a (carrier $ product a (carrier terminal))
+>   rightUnitorInverse a = challenger $ Product.exists (product a (carrier terminal))
+>                                                      a
+>                                                      (identity cat a)
+>                                                      (exists terminal a)
+>
+  
+  doesn't seem necessary
+ 
+  potentialIdentity :
+       (a : obj cat)
+    -> mor cat (carrier $ product a (carrier terminal)) (carrier $ product a (carrier terminal))
+  potentialIdentity a = compose cat
+              (carrier $ product a (carrier terminal))
+              a
+              (carrier $ product a (carrier terminal))
+              (pi1 $ product a (carrier terminal))
+              (challenger (exists (product a (carrier terminal)) a (identity cat a) (exists terminal a)))
+
+>
+>   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
+>   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a)
+>     (rewrite sym $ productPi12Identity a (carrier terminal) in 
+>      Product.unique 
+>             (product a (carrier terminal))
+>             (carrier $ product a (carrier terminal)) 
+>             (pi1 $ product a (carrier terminal)) 
+>             (pi2 $ product a (carrier terminal))
+>             (MkCommutingMorphism 
+>                (compose cat
+>                        (carrier $ product a (carrier terminal))
+>                         a
+>                        (carrier $ product a (carrier terminal))
+>                        (pi1 $ product a (carrier terminal))
+>                        (challenger $ exists (product a (carrier terminal)) a (identity cat a) (exists terminal a))
+>                ) 
+>                (rewrite sym $ associativity cat (carrier $ product a (carrier terminal))
+>                                                  a
+>                                                 (carrier $ product a (carrier terminal)) 
+>                                                  a 
+>                                                 (pi1 $ product a (carrier terminal))
+>                                                 (challenger (exists (product a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                                                 (pi1 $ product a (carrier terminal)) in
+>                 rewrite commutativityLeft $ Product.exists (product a (carrier terminal)) a (identity cat a) (exists terminal a) in
+>                 rightIdentity cat (carrier $ product a (carrier terminal)) a (pi1 $ product a (carrier terminal))
+>                ) 
+>                (TerminalObject.unique terminal (carrier $ product a (carrier terminal)) 
+>                   (compose cat
+>                           (carrier $ product a (carrier terminal))
+>                           (carrier $ product a (carrier terminal))
+>                           (carrier terminal)
+>                           (compose cat
+>                                    (carrier $ product a (carrier terminal))
+>                                    a
+>                                    (carrier $ product a (carrier terminal))
+>                                    (pi1 $ product a (carrier terminal))
+>                                    (challenger $ exists (product a (carrier terminal)) a (identity cat a) (exists terminal a)))
+>                           (pi2 $ product a (carrier terminal)))
+>                  (pi2 $ product a (carrier terminal))
+>                )
+>           )
+>     )
+>     (commutativityLeft $ Product.exists (product a (carrier terminal)) a (identity cat a) (exists terminal a))
+>
+>   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat product) (carrier terminal))
+>                                                  (idFunctor cat)
+>   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
+>
+>   leftUnitorComponent : (a : obj cat) -> mor cat (carrier $ product (carrier terminal) a) a
+>   leftUnitorComponent a = Product.pi2 $ product (carrier terminal) a
+>
+>   leftUnitorComm :
+>        (a, b : obj cat)
+>     -> (f : mor cat a b)
+>     -> compose cat _ _ _ (leftUnitorComponent a) f
+>      = compose cat _ _ _ (mapMor (bifunctorRight cat (productFunctor cat product) (carrier terminal)) a b f)
+>                          (leftUnitorComponent b)
+>   leftUnitorComm a b f = 
+>     rewrite
+>       rightIdentity cat (carrier $ product (carrier terminal) a)
+>                         (carrier terminal)
+>                         (pi1 $ product (carrier terminal) a)
+>      in
+>       sym $ commutativityRight (exists (product (carrier terminal) b)
+>                                        (carrier $ product (carrier terminal) a)
+>                                        (pi1 $ product (carrier terminal) a)
+>                                        (compose cat (carrier $ product (carrier terminal) a)
+>                                                     a b
+>                                                     (pi2 $ product (carrier terminal) a)
+>                                                     f))
+>
+>   leftUnitorNatTrans : NaturalTransformation cat cat
+>                                               (bifunctorRight cat (productFunctor cat product) (carrier terminal))
+>                                               (idFunctor cat)
+>   leftUnitorNatTrans = MkNaturalTransformation leftUnitorComponent leftUnitorComm
+>
+>   leftUnitorInverse : (a : obj cat) -> mor cat a (carrier $ product (carrier terminal) a)
+>   leftUnitorInverse a = challenger $ Product.exists (product (carrier terminal) a)
+>                                                     a
+>                                                     (exists terminal a)
+>                                                     (identity cat a)
+>
+>   leftUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (leftUnitorComponent a)
+>   leftUnitorIsomorphism a = MkIsomorphism (leftUnitorInverse a) 
+>     (rewrite sym $ productPi12Identity (carrier terminal) a in 
+>      Product.unique 
+>             (product (carrier terminal) a)
+>             (carrier $ product (carrier terminal) a) 
+>             (pi1 $ product (carrier terminal) a) 
+>             (pi2 $ product (carrier terminal) a)
+>             (MkCommutingMorphism 
+>                (compose cat
+>                         (carrier $ product (carrier terminal) a)
+>                         a
+>                         (carrier $ product (carrier terminal) a)
+>                         (pi2 $ product (carrier terminal) a)
+>                         (challenger $ exists (product (carrier terminal) a) a (exists terminal a) (identity cat a))
+>                )
+>                (TerminalObject.unique terminal (carrier $ product (carrier terminal) a) 
+>                   (compose cat
+>                           (carrier $ product (carrier terminal) a)
+>                           (carrier $ product (carrier terminal) a)
+>                           (carrier terminal)
+>                           (compose cat
+>                                    (carrier $ product (carrier terminal) a)
+>                                    a
+>                                    (carrier $ product (carrier terminal) a)
+>                                    (pi2 $ product (carrier terminal) a)
+>                                    (challenger $ exists (product (carrier terminal) a) a (exists terminal a) (identity cat a)))
+>                           (pi1 $ product (carrier terminal) a))
+>                  (pi1 $ product (carrier terminal) a)
+>                )
+>                (rewrite sym $ associativity cat (carrier $ product (carrier terminal) a)
+>                                                  a
+>                                                 (carrier $ product (carrier terminal) a) 
+>                                                  a 
+>                                                 (pi2 $ product (carrier terminal) a)
+>                                                 (challenger $ exists (product (carrier terminal) a) a (exists terminal a) (identity cat a))
+>                                                 (pi2 $ product (carrier terminal) a) in
+>                 rewrite commutativityRight $ Product.exists (product (carrier terminal) a) a (exists terminal a) (identity cat a)  in
+>                 rightIdentity cat (carrier $ product (carrier terminal) a) a (pi2 $ product (carrier terminal) a)
+>                )
+>             )
+>     ) 
+>     (commutativityRight $ Product.exists (product (carrier terminal) a) a (exists terminal a) (identity cat a))
+>
+>   leftUnitorNatIso : NaturalIsomorphism cat cat (bifunctorRight cat (productFunctor cat product) (carrier terminal))
+>                                                 (idFunctor cat)
+>   leftUnitorNatIso = MkNaturalIsomorphism leftUnitorNatTrans leftUnitorIsomorphism
+>
+>   infixr 4 <**>
+>
+>   (<**>) : obj cat -> obj cat -> obj cat
+>   (<**>) a b = carrier $ product a b
+> 
+>   associatorComponent : (a, b, c : obj cat) -> mor cat ((a <**> b) <**> c) (a <**> (b <**> c))
+>   associatorComponent a b c = 
+>     challenger $ Product.exists (product a (b <**> c)) ((a <**> b) <**> c) 
+>       (compose cat ((a <**> b) <**> c) (a <**> b) a 
+>                    (pi1 $ product (a <**> b) c) 
+>                    (pi1 $ product a b))
+>       (challenger $ Product.exists (product b c) ((a <**> b) <**> c)
+>        (compose cat ((a <**> b) <**> c) (a <**> b) b
+>                     (pi1 $ product (a <**> b) c) 
+>                     (pi2 $ product a b))
+>        (pi2 $ product (a <**> b) c))
+>
+>   associatorInvComponent : (a, b, c : obj cat) -> mor cat (a <**> (b <**> c)) ((a <**> b) <**> c) 
+>   associatorInvComponent a b c = 
+>     challenger $ Product.exists (product (a <**> b) c) (a <**> (b <**> c)) 
+>       (challenger $ Product.exists (product a b) (a <**> (b <**> c))
+>        (pi1 $ product a (b <**> c))
+>        (compose cat (a <**> (b <**> c)) (b <**> c) b
+>                     (pi2 $ product a (b <**> c)) 
+>                     (pi1 $ product b c)))
+>       (compose cat (a <**> (b <**> c)) (b <**> c) c 
+>                    (pi2 $ product a (b <**> c)) 
+>                    (pi2 $ product b c))
+
+* Prove they are isomorphisms (Horrible)
+* Prove they define a natural transformation
+* Prove Triangle identity
+* Prove Pentagon identity (Horrible too) 
+
diff --git a/src/Limits/Product.lidr b/src/Limits/Product.lidr
index 151a1be..e485eb2 100644
--- a/src/Limits/Product.lidr
+++ b/src/Limits/Product.lidr
@@ -23,11 +23,7 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > import Basic.Category
 > import Basic.Functor
-> import Basic.Isomorphism
-> import Basic.NaturalTransformation
-> import Basic.NaturalIsomorphism
 > import Product.ProductCategory
-> import Limits.TerminalObject
 >
 > %access public export
 > %default total
@@ -77,51 +73,51 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >
 > productFunctor :
 >      (cat : Category)
->   -> (productObj : catHasProducts cat)
+>   -> (product : catHasProducts cat)
 >   -> CFunctor (productCategory cat cat) cat
-> productFunctor cat productObj = MkCFunctor mapObj mapMor idLaw compLaw
+> productFunctor cat product = MkCFunctor mapObj mapMor idLaw compLaw
 >   where
 >     mapObj : (obj cat, obj cat) -> obj cat
->     mapObj (a,b) = carrier $ productObj a b
+>     mapObj (a,b) = carrier $ product a b
 >     mapMor :
 >          (a, b : obj (productCategory cat cat))
 >       -> mor (productCategory cat cat) a b
 >       -> mor cat (mapObj a) (mapObj b)
 >     mapMor (a1,b1) (a2,b2) (MkProductMorphism f g) =
->       productMorphism cat a1 a2 b1 b2 f g (productObj a1 b1) (productObj a2 b2)
+>       productMorphism cat a1 a2 b1 b2 f g (product a1 b1) (product a2 b2)
 >     identityCommutingMorphism :
 >          (a,b : obj cat)
 >       -> CommutingMorphism cat
->                            (carrier (productObj a b)) a b (carrier (productObj a b))
->                            (pi1 (productObj a b)) (pi2 (productObj a b))
->                            (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
->                            (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
+>                            (carrier (product a b)) a b (carrier (product a b))
+>                            (pi1 (product a b)) (pi2 (product a b))
+>                            (compose cat (carrier (product a b)) a a (pi1 (product a b)) (identity cat a))
+>                            (compose cat (carrier (product a b)) b b (pi2 (product a b)) (identity cat b))
 >     identityCommutingMorphism a b =
->       MkCommutingMorphism (identity cat (carrier (productObj a b)))
->                           (rewrite leftIdentity cat (carrier (productObj a b)) a (pi1 (productObj a b)) in
->                             sym $ rightIdentity cat (carrier (productObj a b)) a (pi1 (productObj a b)))
->                           (rewrite leftIdentity cat (carrier (productObj a b)) b (pi2 (productObj a b)) in
->                             sym $ rightIdentity cat (carrier (productObj a b)) b (pi2 (productObj a b)))
+>       MkCommutingMorphism (identity cat (carrier (product a b)))
+>                           (rewrite leftIdentity cat (carrier (product a b)) a (pi1 (product a b)) in
+>                             sym $ rightIdentity cat (carrier (product a b)) a (pi1 (product a b)))
+>                           (rewrite leftIdentity cat (carrier (product a b)) b (pi2 (product a b)) in
+>                             sym $ rightIdentity cat (carrier (product a b)) b (pi2 (product a b)))
 >     idLaw :
 >          (a : obj (productCategory cat cat))
 >       -> mapMor a a (identity (productCategory cat cat) a) = identity cat (mapObj a)
->     idLaw (a,b) = sym $ unique (productObj a b)
->                                (carrier (productObj a b))
->                                (compose cat (carrier (productObj a b)) a a (pi1 (productObj a b)) (identity cat a))
->                                (compose cat (carrier (productObj a b)) b b (pi2 (productObj a b)) (identity cat b))
+>     idLaw (a,b) = sym $ unique (product a b)
+>                                (carrier (product a b))
+>                                (compose cat (carrier (product a b)) a a (pi1 (product a b)) (identity cat a))
+>                                (compose cat (carrier (product a b)) b b (pi2 (product a b)) (identity cat b))
 >                                (identityCommutingMorphism a b)
 >     compComMor : (a1,a2,b1,b2,c1,c2 : obj cat) 
 >               -> (f1 : mor cat a1 b1) -> (f2 : mor cat a2 b2) 
 >               -> (g1 : mor cat b1 c1) -> (g2 : mor cat b2 c2)
->               -> CommutingMorphism cat (carrier (productObj a1 a2)) c1 c2 
->                                    (carrier (productObj c1 c2)) (pi1 (productObj c1 c2)) (pi2 (productObj c1 c2)) 
->                                    (compose cat (carrier (productObj a1 a2)) a1 c1 (pi1 (productObj a1 a2)) (compose cat a1 b1 c1 f1 g1))
->                                    (compose cat (carrier (productObj a1 a2)) a2 c2 (pi2 (productObj a1 a2)) (compose cat a2 b2 c2 f2 g2))
+>               -> CommutingMorphism cat (carrier (product a1 a2)) c1 c2 
+>                                    (carrier (product c1 c2)) (pi1 (product c1 c2)) (pi2 (product c1 c2)) 
+>                                    (compose cat (carrier (product a1 a2)) a1 c1 (pi1 (product a1 a2)) (compose cat a1 b1 c1 f1 g1))
+>                                    (compose cat (carrier (product a1 a2)) a2 c2 (pi2 (product a1 a2)) (compose cat a2 b2 c2 f2 g2))
 >     compComMor a1 a2 b1 b2 c1 c2 f1 f2 g1 g2 = 
 >       let 
->         pa = productObj a1 a2
->         pb = productObj b1 b2
->         pc = productObj c1 c2
+>         pa = product a1 a2
+>         pb = product b1 b2
+>         pc = product c1 c2
 >         cmab = exists pb (carrier pa) (compose cat (carrier pa) a1 b1 (pi1 pa) f1)
 >                                       (compose cat (carrier pa) a2 b2 (pi2 pa) f2)
 >         cmbc = exists pc (carrier pb) (compose cat (carrier pb) b1 c1 (pi1 pb) g1)
@@ -151,15 +147,12 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >          mapMor a c (productCompose a b c f g) =
 >          compose cat (mapObj a) (mapObj b) (mapObj c) (mapMor a b f) (mapMor b c g)
 >     compLaw (a1,a2) (b1,b2) (c1,c2) (MkProductMorphism f1 f2) (MkProductMorphism g1 g2) = 
->       sym $ unique (productObj c1 c2) 
->                    (carrier (productObj a1 a2)) 
->                    (compose cat (carrier (productObj a1 a2)) a1 c1 (pi1 (productObj a1 a2)) (compose cat a1 b1 c1 f1 g1))
->                    (compose cat (carrier (productObj a1 a2)) a2 c2 (pi2 (productObj a1 a2)) (compose cat a2 b2 c2 f2 g2))
+>       sym $ unique (product c1 c2) 
+>                    (carrier (product a1 a2)) 
+>                    (compose cat (carrier (product a1 a2)) a1 c1 (pi1 (product a1 a2)) (compose cat a1 b1 c1 f1 g1))
+>                    (compose cat (carrier (product a1 a2)) a2 c2 (pi2 (product a1 a2)) (compose cat a2 b2 c2 f2 g2))
 >                    (compComMor a1 a2 b1 b2 c1 c2 f1 f2 g1 g2)
 >
-> catHasTerminalObj : Category -> Type
-> catHasTerminalObj = TerminalObject
->
 > bifunctorLeft :
 >      (cat : Category)
 >   -> (fun : CFunctor (productCategory cat cat) cat)
@@ -237,207 +230,4 @@ along with this program.  If not, see <https://www.gnu.org/licenses/>.
 >                                    (mapMor (a, y) (a, z) (MkProductMorphism (identity cat a) g))}
 >               (rightIdentity cat a a (identity cat a))
 >               (pComp (a,x) (a,y) (a,z) (MkProductMorphism (identity cat a) f) (MkProductMorphism (identity cat a) g))
->
-> parameters (cat : Category, products : catHasProducts cat, terminal : catHasTerminalObj cat)
->   commutativeIdentity :
->        (a, b : obj cat)
->     -> let pab = products a b in
->        CommutingMorphism cat (carrier pab) a b (carrier pab) (pi1 pab) (pi2 pab) (pi1 pab) (pi2 pab)
->   commutativeIdentity a b =
->     MkCommutingMorphism (identity cat $ carrier $ products a b)
->                         (leftIdentity cat (carrier $ products a b) a (pi1 $ products a b))
->                         (leftIdentity cat (carrier $ products a b) b (pi2 $ products a b))
->
->   productPi12Identity :
->        (a, b : obj cat)
->     -> let pab = products a b in
->        challenger $ Product.exists pab (carrier pab) (pi1 pab) (pi2 pab) = identity cat (carrier pab)
->   productPi12Identity a b = sym $ unique (products a b)
->                                          (carrier $ products a b)
->                                          (pi1 $ products a b)
->                                          (pi2 $ products a b)
->                                          (commutativeIdentity a b)
->
->   rightUnitorComponent : (a : obj cat) -> mor cat (carrier $ products a (carrier terminal)) a
->   rightUnitorComponent a = Product.pi1 $ products a (carrier terminal)
->
->   rightUnitorComm :
->        (a, b : obj cat)
->     -> (f : mor cat a b)
->     -> compose cat _ _ _ (rightUnitorComponent a) f
->      = compose cat _ _ _ (mapMor (bifunctorLeft cat (productFunctor cat products) (carrier terminal)) a b f)
->                          (rightUnitorComponent b)
->   rightUnitorComm a b f =
->     rewrite
->       rightIdentity cat (carrier $ products a (carrier terminal))
->                         (carrier terminal)
->                         (pi2 $ products a (carrier terminal))
->     in
->       sym $ commutativityLeft (exists (products b (carrier terminal))
->                                       (carrier $ products a (carrier terminal))
->                                       (compose cat (carrier $ products a (carrier terminal))
->                                                    a b
->                                                    (pi1 $ products a (carrier terminal))
->                                                    f)
->                                       (pi2 $ products a (carrier terminal)))
->
->   rightUnitorNatTrans : NaturalTransformation cat cat
->                                               (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
->                                               (idFunctor cat)
->   rightUnitorNatTrans = MkNaturalTransformation rightUnitorComponent rightUnitorComm
->
->   rightUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products a (carrier terminal))
->   rightUnitorInverse a = challenger $ Product.exists (products a (carrier terminal))
->                                                      a
->                                                      (identity cat a)
->                                                      (exists terminal a)
->
-  
-  doesn't seem necessary
- 
-  potentialIdentity :
-       (a : obj cat)
-    -> mor cat (carrier $ products a (carrier terminal)) (carrier $ products a (carrier terminal))
-  potentialIdentity a = compose cat
-              (carrier $ products a (carrier terminal))
-              a
-              (carrier $ products a (carrier terminal))
-              (pi1 $ products a (carrier terminal))
-              (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
-
->
->   rightUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (rightUnitorComponent a)
->   rightUnitorIsomorphism a = MkIsomorphism (rightUnitorInverse a)
->     (rewrite sym $ productPi12Identity a (carrier terminal) in 
->      Product.unique 
->             (products a (carrier terminal))
->             (carrier $ products a (carrier terminal)) 
->             (pi1 $ products a (carrier terminal)) 
->             (pi2 $ products a (carrier terminal))
->             (MkCommutingMorphism 
->                (compose cat
->                        (carrier $ products a (carrier terminal))
->                         a
->                        (carrier $ products a (carrier terminal))
->                        (pi1 $ products a (carrier terminal))
->                        (challenger $ exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
->                ) 
->                (rewrite sym $ associativity cat (carrier $ products a (carrier terminal))
->                                                  a
->                                                 (carrier $ products a (carrier terminal)) 
->                                                  a 
->                                                 (pi1 $ products a (carrier terminal))
->                                                 (challenger (exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
->                                                 (pi1 $ products a (carrier terminal)) in
->                 rewrite commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a) in
->                 rightIdentity cat (carrier $ products a (carrier terminal)) a (pi1 $ products a (carrier terminal))
->                ) 
->                (TerminalObject.unique terminal (carrier $ products a (carrier terminal)) 
->                   (compose cat
->                           (carrier $ products a (carrier terminal))
->                           (carrier $ products a (carrier terminal))
->                           (carrier terminal)
->                           (compose cat
->                                    (carrier $ products a (carrier terminal))
->                                    a
->                                    (carrier $ products a (carrier terminal))
->                                    (pi1 $ products a (carrier terminal))
->                                    (challenger $ exists (products a (carrier terminal)) a (identity cat a) (exists terminal a)))
->                           (pi2 $ products a (carrier terminal)))
->                  (pi2 $ products a (carrier terminal))
->                )
->           )
->     )
->     (commutativityLeft $ Product.exists (products a (carrier terminal)) a (identity cat a) (exists terminal a))
->
->   rightUnitorNatIso : NaturalIsomorphism cat cat (bifunctorLeft cat (productFunctor cat products) (carrier terminal))
->                                                  (idFunctor cat)
->   rightUnitorNatIso = MkNaturalIsomorphism rightUnitorNatTrans rightUnitorIsomorphism
->
->   leftUnitorComponent : (a : obj cat) -> mor cat (carrier $ products (carrier terminal) a) a
->   leftUnitorComponent a = Product.pi2 $ products (carrier terminal) a
->
->   leftUnitorComm :
->        (a, b : obj cat)
->     -> (f : mor cat a b)
->     -> compose cat _ _ _ (leftUnitorComponent a) f
->      = compose cat _ _ _ (mapMor (bifunctorRight cat (productFunctor cat products) (carrier terminal)) a b f)
->                          (leftUnitorComponent b)
->   leftUnitorComm a b f = 
->     rewrite
->       rightIdentity cat (carrier $ products (carrier terminal) a)
->                         (carrier terminal)
->                         (pi1 $ products (carrier terminal) a)
->      in
->       sym $ commutativityRight (exists (products (carrier terminal) b)
->                                        (carrier $ products (carrier terminal) a)
->                                        (pi1 $ products (carrier terminal) a)
->                                        (compose cat (carrier $ products (carrier terminal) a)
->                                                     a b
->                                                     (pi2 $ products (carrier terminal) a)
->                                                     f))
->
->   leftUnitorNatTrans : NaturalTransformation cat cat
->                                               (bifunctorRight cat (productFunctor cat products) (carrier terminal))
->                                               (idFunctor cat)
->   leftUnitorNatTrans = MkNaturalTransformation leftUnitorComponent leftUnitorComm
->
->   leftUnitorInverse : (a : obj cat) -> mor cat a (carrier $ products (carrier terminal) a)
->   leftUnitorInverse a = challenger $ Product.exists (products (carrier terminal) a)
->                                                     a
->                                                     (exists terminal a)
->                                                     (identity cat a)
->
->   leftUnitorIsomorphism : (a : obj cat) -> Isomorphism cat _ _ (leftUnitorComponent a)
->   leftUnitorIsomorphism a = MkIsomorphism (leftUnitorInverse a) 
->     (rewrite sym $ productPi12Identity (carrier terminal) a in 
->      Product.unique 
->             (products (carrier terminal) a)
->             (carrier $ products (carrier terminal) a) 
->             (pi1 $ products (carrier terminal) a) 
->             (pi2 $ products (carrier terminal) a)
->             (MkCommutingMorphism 
->                (compose cat
->                         (carrier $ products (carrier terminal) a)
->                         a
->                         (carrier $ products (carrier terminal) a)
->                         (pi2 $ products (carrier terminal) a)
->                         (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
->                )
->                (TerminalObject.unique terminal (carrier $ products (carrier terminal) a) 
->                   (compose cat
->                           (carrier $ products (carrier terminal) a)
->                           (carrier $ products (carrier terminal) a)
->                           (carrier terminal)
->                           (compose cat
->                                    (carrier $ products (carrier terminal) a)
->                                    a
->                                    (carrier $ products (carrier terminal) a)
->                                    (pi2 $ products (carrier terminal) a)
->                                    (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a)))
->                           (pi1 $ products (carrier terminal) a))
->                  (pi1 $ products (carrier terminal) a)
->                )
->                (rewrite sym $ associativity cat (carrier $ products (carrier terminal) a)
->                                                  a
->                                                 (carrier $ products (carrier terminal) a) 
->                                                  a 
->                                                 (pi2 $ products (carrier terminal) a)
->                                                 (challenger $ exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
->                                                 (pi2 $ products (carrier terminal) a) in
->                 rewrite commutativityRight $ Product.exists (products (carrier terminal) a) a (exists terminal a) (identity cat a)  in
->                 rightIdentity cat (carrier $ products (carrier terminal) a) a (pi2 $ products (carrier terminal) a)
->                )
->             )
->     ) 
->     (commutativityRight $ Product.exists (products (carrier terminal) a) a (exists terminal a) (identity cat a))
->
->   leftUnitorNatIso : NaturalIsomorphism cat cat (bifunctorRight cat (productFunctor cat products) (carrier terminal))
->                                                 (idFunctor cat)
->   leftUnitorNatIso = MkNaturalIsomorphism leftUnitorNatTrans leftUnitorIsomorphism
-
-* Define associator components: (A x B) x C --> A x (B x C)
-* Prove they are isomorphisms (Horrible)
-* Prove they define a natural transformation
-* Prove Triangle identity
-* Prove Pentagon identity (Horrible too) 
\ No newline at end of file
+>
\ No newline at end of file