This is a Coq formalisation of Selective Applicative Functors, containing proof of Functor, Applicative and Selective laws for a number of instances.
To play with the definitions and proofs, you'll need to have the Coq proof assistant installed. You will also need the Equations plug-in. The proofs can be checked by running make.
The most interesting thing in this repo is the data type formalising free rigid selective functors
Inductive Select (F : Type -> Type) (A : Type) :=
Pure : A -> Select F A
| MkSelect : forall B, Select F (B + A) -> F (B -> A) -> Select F A.
and the proofs it is a lawful instance of Functor, Applicative and (proof to be completed) Selective.
The proofs for free rigid selective functors rely no three free theorems which
hold by parametricity and admitted as axioms. See SelectiveParametricity for details. We also reformulate these theorems for the data constructor MkSelect
We borrowed a number of definitions and tricks from @jwiegley's coq-haskell library.