{-# OPTIONS --cubical-compatible #-}
module Terra.Classes.Contravariant where
open import Terra.Data.Level


record Contravariant {ℓ} (F : Set ℓ -> Set ℓ) : Set (lsuc ℓ) where
  field
    contramap : {A B : Set ℓ} -> (B -> A) -> F A -> F B

open Contravariant {{...}} public