Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

WIP, Liveshare: Limits #28

Open
wants to merge 13 commits into
base: master
Choose a base branch
from
Open

WIP, Liveshare: Limits #28

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
0484b6f
split TerminalObject and Product into separate files
marcosh Jun 3, 2019
794372f
prove that terminal objects are isomorphic
marcosh Jun 4, 2019
34049f8
live sharing session
wires Jun 6, 2019
daf4928
useless fixes
marcosh Jun 10, 2019
f3454e7
liveshare
Jun 13, 2019
ae5b646
clean code of shared coding session
marcosh Jun 17, 2019
569595b
liveshare
wires Jun 20, 2019
55459cb
fix style
marcosh Jun 27, 2019
c124b7d
live session 11.07.2019
clayrat Jul 11, 2019
ff8efe9
dualize for left unitor
clayrat Jul 20, 2019
aa93f17
prove compLaw
clayrat Jul 24, 2019
2c83299
prettify compLaw
clayrat Jul 24, 2019
f60b6e2
live session 25.07.2019
clayrat Jul 25, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 3 additions & 0 deletions idris-ct.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,9 @@ modules =
Idris.FunctorAsCFunctor,
Idris.TypesAsCategory,
Idris.TypesAsCategoryExtensional,
Limits.TerminalObject,
Limits.Product,
Limits.MonoidalProduct,
Monoid.Monoid,
Monoid.MonoidAsCategory,
Monoid.MonoidMorphism,
Expand Down
5 changes: 1 addition & 4 deletions src/CoLimits/CoProduct.lidr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
268 changes: 268 additions & 0 deletions src/Limits/MonoidalProduct.lidr
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)

Loading