module Stdlib.Trait.Functor.Polymorphic;
import Stdlib.Data.Fixity open;
import Stdlib.Data.Unit open;
trait
type Functor (f : Type -> Type) :=
mkFunctor {
syntax iterator map {init := 0; range := 1};
map : {A B : Type} -> (A -> B) -> f A -> f B
};
open Functor public;
syntax operator <$> lapp;
<$> {f : Type -> Type} {{Functor f}} {A B} : (A -> B) -> f A -> f B := map;
syntax operator $> lapp;
$> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B :=
λ {_ := b} <$> fa;
void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit :=
fa $> unit;