ContraFunctor properties

Changes

1 changed files (+4/-0)

• Dao.lean
  • @@ -165,6 +165,10 @@ end Yoneda
    class ContraFunctor (f : Type → Type) where contramap : (β → α) → f α → f β + id_contramap (x : f α) : contramap id x = x + comp_contramap (g : β → α) (h : γ → β) (x : f α) : contramap (g ∘ h) x = contramap h (contramap g x) instance (α : Type) : ContraFunctor (· → α) where contramap f g := fun x ↦ g (f x) + id_contramap := by simp + comp_contramap := by simp