This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Given distributive category | |
* -C>, >C<, 1C, +C+, 0C | |
And monoidal category | |
* -D>, >D<, 1D | |
A lax alternative functor consists of | |
* A functor | |
- F : C -> D | |
* morphisms | |
- eps : 1D -D> F(1C) | |
- mu : F(a) >D< F(b) -D> F(a >C< b) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** Coq proof that there is no monad compatible with the ZipList applicative functor. *) | |
(** Based on the original proof by Koji Miyazato https://gist.github.com/viercc/38853067c893f7ad9e0894abb543178b *) | |
(** Main theorem: [No_LawfulJoin : forall join, ~(LawfulJoin join)] | |
where [~] means "not" and [LawfulJoin] is the conjunction of the following properties (monad laws): | |
1. [join] is associative: | |
join (join xs) = join (map join xs)] | |
2. [join] is compatible with ZipList's applicative (i.e., [zip_with]): |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- Based on: http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html | |
import Data.List (delete, union) | |
{- HLINT ignore "Eta reduce" -} | |
-- File mnemonics: | |
-- env = typing environment | |
-- vid = variable identifier in Bind or Var | |
-- br = binder variant (Lambda or Pi) | |
-- xyzTyp = type of xyz | |
-- body = body of Lambda or Pi abstraction |