functor

Functor package contains functor implementation and laws packed in Sigma container.

Signature

fmap_sig (F: U -> U) : U = (A B: U) -> (A -> B) -> F A -> F B

Type Class

functor: U = (F: U -> U) * fmap_sig F

Properties

The package also contains proof-free code for runtime facilities.

isFunctor (F: functor): U
    = (id: (A: U) -> (x: F.1 A) -> Path (F.1 A) (fmap F A A (idfun A) x) x)
    * (compose: (A B C: U) (f: B -> C) (g: A -> B) (x: F.1 A) ->
      Path (F.1 C) (F.2 A C (o A B C f g) x)
       ((o (F.1 A) (F.1 B) (F.1 C)
           (F.2 B C f) (F.2 A B g)) x)) * unit
                functor (A B: U) (F: U -> U): U
                    = (fmap: (A -> B) -> F A -> F B) * unit

FUNCTOR: U = (f: functor) * isFunctor f

Functor Instances

functor_id: FUNCTOR = ((\(A:U)->A,apply),(id,compose,tt)) where
  id: (A: U) -> (a: A) -> Path A a a = refl
  compose (A B C: U) (f: B->C) (g: A->B) (x: A):
     Path C (f(g(x))) (f(g(x))) = refl C (o A B C f g x)

functor_const (A: U): FUNCTOR = ((const A,fmap),(id,compose,tt)) where
  fmap (B C: U) (_: B -> C): A -> A = idfun A
  id (_ : U): (x : A) -> Path A x x = refl A
  compose (X B C: U) (f: B->C) (g: X->B): (x: A) -> Path A x x = refl A

functor_fun (T: U): FUNCTOR = ((\(B:U)->T->B,fmap),(id,compose,tt)) where
  fmap (A B: U) (map: A -> B): (T -> A) -> (T -> B) = o T A B map
  id (A: U): (x: T->A) -> Path (T->A) x x = refl (T->A)
  compose (A B C: U) (f: B->C) (g: A->B) (x: T->A):
     Path (T->C) (\(y: T) -> f (g (x y)))
                 (\(y: T) -> f (g (x y)))
   = refl (T->C) (\(y: T) -> f (g (x y)))

functor_comptype (f g: FUNCTOR): FUNCTOR
   = ((funcomp F G,fmap),(id,compose,tt)) where ...