theory.functors

Require Import
  canonical_names abstract_algebra
  interfaces.functors.
Require
  categories.setoids.

Section setoid_functor_as_posh_functor.

  Context `{SFunctor F}.

  Program Definition map_setoid: setoids.Object setoids.Object :=
    λ o, @setoids.object (F (setoids.T o)) (map_eq (setoids.T o) (setoids.e o)) _.


  Program Instance: Fmap map_setoid := λ v w X, @sfmap F H _ _ (proj1_sig X).


  Instance: Functor map_setoid _.

End setoid_functor_as_posh_functor.

Note that we cannot prove the reverse (i.e. that an endo-Functor on setoid.Object gives rise to an SFunctor, because an SFunctor requires a Type→Type map, which we cannot get from a setoid.Object→setoid.Object map.