File: FunctorLaws.v

package info (click to toggle)
coq-ext-lib 0.13.0-3
  • links: PTS, VCS
  • area: main
  • in suites: experimental
  • size: 808 kB
  • sloc: makefile: 44; python: 31; sh: 4; lisp: 3
file content (16 lines) | stat: -rw-r--r-- 444 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
From Coq.Relations Require Import Relations.
Require Import ExtLib.Data.Fun.
Require Import ExtLib.Structures.Functor.

Set Implicit Arguments.
Set Strict Implicit.
Set Universe Polymorphism.

Section laws.

  Class FunctorLaws {F} (Functor_F : Functor F) :=
  { fmap_id : forall {T} (x : F T), fmap id x = x
  ; fmap_compose : forall {T U V} (f : T -> U) (g : U -> V) (x : F T),
        fmap (compose g f) x = fmap g (fmap f x)
  }.
End laws.