class Data.Functor.Contravariant (F : Type u → Type v) : Type (max (u + 1) v)

A contravariant functor $F : \mathsf{Type}^{\text{op}} \to \mathsf{Type}$. Unlike a covariant functor which preserves morphism direction, a contravariant functor reverses it: given $f : \alpha \to \beta$, we obtain

$$\text{contramap}\; f : F\;\beta \to F\;\alpha$$

• contramap {α β : Type u} : (α → β) → F β → F α

  Map contravariantly: given $f : \alpha \to \beta$, produce $\text{contramap}\;f : F\;\beta \to F\;\alpha$.

class Data.Functor.LawfulContravariant (F : Type u → Type v) [Contravariant F] : Prop

Laws for a lawful contravariant functor:

1. Identity: $\text{contramap}\;\text{id} = \text{id}$
2. Composition: $\text{contramap}\;(f \circ g) = \text{contramap}\;g \circ \text{contramap}\;f$

Note the reversal in the composition law — this is dual to the covariant functor law.

• contramap_id {α : Type u} (x : F α) : Contravariant.contramap id x = x

  Identity law: $\text{contramap}\;\text{id}\;x = x$.

• contramap_comp {β γ α : Type u} (f : β → γ) (g : α → β) (x : F γ) : Contravariant.contramap (f ∘ g) x = Contravariant.contramap g (Contravariant.contramap f x)

  Composition law: $\text{contramap}\;(f \circ g)\;x = \text{contramap}\;g\;(\text{contramap}\;f\;x)$.

structure Data.Functor.Predicate (α : Type u) : Type u

A predicate $P : \alpha \to \text{Prop}$, wrapped as a contravariant functor.

Given $f : \alpha \to \beta$ and a predicate $P$ on $\beta$, the contramapped predicate is $P \circ f$, i.e., $(\text{contramap}\;f\;P)(x) = P(f(x))$.

• getPredicate : α → Prop

@[implicit_reducible]

instance Data.Functor.instContravariantPredicate : Contravariant Predicate

Contravariant instance for Predicate: $\text{contramap}\;f\;P = P \circ f$.

Equations

• Data.Functor.instContravariantPredicate = { contramap := fun {α β : Type ?u.10} (f : α → β) (p : Data.Functor.Predicate β) => { getPredicate := p.getPredicate ∘ f } }

instance Data.Functor.instLawfulContravariantPredicate : LawfulContravariant Predicate

Predicate is a lawful contravariant functor — both laws hold definitionally.

structure Data.Functor.Equivalence (α : Type u) : Type u

An equivalence relation $R : \alpha \to \alpha \to \text{Prop}$, wrapped as a contravariant functor.

Given $f : \alpha \to \beta$ and an equivalence $R$ on $\beta$, the contramapped equivalence is: $(\text{contramap}\;f\;R)(a, b) = R(f(a), f(b))$.

• getEquivalence : α → α → Prop

@[implicit_reducible]

instance Data.Functor.instContravariantEquivalence : Contravariant Equivalence

Contravariant instance for Equivalence: $(\text{contramap}\;f\;R)(a, b) = R(f(a),\, f(b))$.

Equations

• One or more equations did not get rendered due to their size.

instance Data.Functor.instLawfulContravariantEquivalence : LawfulContravariant Equivalence

Equivalence is a lawful contravariant functor — both laws hold definitionally.