Contravariant functor

Stream: Is there code for X?

[Léo Lessa]

Does mathlib have a "contravariant functor" class (outside CategoryTheory), akin to Haskell's Contravariant? That is, something like:

class ContravariantFunctor (f : Type u → Type v) where
  contramap : {α β : Type u} → (α → β) → f β → f α

[Edward van de Meent]

@loogle "contravariant"

[loogle]

:search: Contravariant, ContravariantClass, and 42 more

[Adam Topaz]

I don’t think we have this

[Edward van de Meent]

From the looks of it, we don't, no. We only seem to have contravariant relations(?)

[Chris Wong]

What's your use case for the class? If it's composing comparison functions, you might be interested in onFun

[Chris Wong]

@loogle onFun

[loogle]

:exclamation: unknown identifier 'onFun'
Did you mean "onFun", Function.onFun, or something else?

[Léo Lessa]

A generic use case could be to characterize classes Class (i : Type u) whose methods functorially depend on a type i as input. For example, the class

class ExampleClass (i : Type u) where
  method1 : i → ℕ
  ...

could be an instance of ContravariantFunctor as

instance inst : ContravariantFunctor ExampleClass where
  contramap (f : i → j) ej := { method1 : j → ℕ := ej.method1 ∘ f, ...}

I personally encountered a case just like the one above when defining a congr theorem here. In that case, it should have followed that, if f is a contravariant functor, then α ≃ β implies f α ≃ f β, which would be the contravariant version of Functor.mapEquiv. Instead, I had to write it by hand.