{-# OPTIONS --without-K #-}
module Class.Functor.Core where
 
open import Class.Prelude
open import Class.Core
 
private variable a b c : Level
 
record Functor (F : Type↑) : Typeω where
  infixl  _<$>_ _<$_
  infixl  _<&>_
 
  field _<$>_ : (A → B) → F A → F B
  fmap = _<$>_
 
  _<$_ : A → F B → F A
  x <$ y = const x <$> y
 
  _<&>_ : F A → (A → B) → F B
  _<&>_ = flip _<$>_
open Functor ⦃...⦄ public
 
record FunctorLaws (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
  field
    -- preserves identity morphisms
    fmap-id : ∀ {A : Type a} (x : F A) →
      fmap id x ≡ x
    -- preserves composition of morphisms
    fmap-∘  : ∀ {A : Type a} {B : Type b} {C : Type c}
                {f : B → C} {g : A → B} (x : F A) →
      fmap (f ∘ g) x ≡ (fmap f ∘ fmap g) x
open FunctorLaws ⦃...⦄ public