https://twitter.com/cutsea110/status/537229738373160961

Test.agda

module Test where

open import Relation.Binary.PropositionalEquality

postulate
  extensionality : ∀ {a} {b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g

covariant : {B : Set} → (B → B → B) → {A : Set} → (A → B) → (A → B) → (A → B)
covariant _⊕_ f g = λ x → f x ⊕ g x

record IsSemiGroup {A : Set} (_∙_ : A → A → A) : Set where
  field
    assoc : ∀ x y z → (x ∙ y) ∙ z ≡ x ∙ (y ∙ z)

theorem : {B : Set} {_⊕_ : B → B → B} → IsSemiGroup _⊕_ → {A : Set} → IsSemiGroup (covariant _⊕_ {A})
theorem sg = record { assoc = λ x y z → extensionality (λ a → IsSemiGroup.assoc sg (x a) (y a) (z a)) }