echatav

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)

Lysxia

(** 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]):

lukaszlew

-- 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