Lawfulness of applicative implementations than compile for homogenous pair

Two.agda

module Two where

open import Level using (Level)
open import Function using (_∘_; id; _$_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎; step-≡; step-≡˘)

data Two (A : Set) : Set where
  TwoOf : A → A → Two A

pure : ∀{a : Set} → a → Two a
pure x = TwoOf x x

-- ONE (lawful)

infixl 5 _<*>¹_

_<*>¹_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b
_<*>¹_ (TwoOf f g) (TwoOf x y) = TwoOf (f x) (g y)

identity¹ : ∀{a : Set} → (v : Two a) → pure id <*>¹ v ≡ v
identity¹ (TwoOf _ _) = refl

composition¹ : ∀{a b c : Set} → (u : Two (b → c)) → (v : Two (a → b)) → (w : Two a)
             → pure (\f g x → f (g x)) <*>¹ u <*>¹ v <*>¹ w ≡ u <*>¹ (v <*>¹ w)
composition¹ (TwoOf _ _) (TwoOf _ _) (TwoOf _ _) = refl

homomorphism¹ : ∀{a b : Set} → (f : a → b) → (x : a)
              → pure f <*>¹ pure x ≡ pure (f x)
homomorphism¹ _ _ = refl

interchange¹ : ∀{a b : Set} → (u : Two (a → b)) → (y : a)
             → u <*>¹ pure y ≡ pure (_$ y) <*>¹ u
interchange¹ (TwoOf _ _) _ = refl

-- TWO (unlawful?)

infixl 5 _<*>²_

_<*>²_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b
_<*>²_ (TwoOf f g) (TwoOf x y) = TwoOf (g x) (f y)

identity² : ∀{a : Set} → (v : Two a) → pure id <*>² v ≡ v
identity² (TwoOf _ _) = refl

composition² : ∀{a b c : Set} → (u : Two (b → c)) → (v : Two (a → b)) → (w : Two a)
             → pure (\f g x → f (g x)) <*>² u <*>² v <*>² w ≡ u <*>² (v <*>² w)
composition² (TwoOf _ _) (TwoOf _ _) (TwoOf _ _) = {!!} -- looks unlawful

homomorphism² : ∀{a b : Set} → (f : a → b) → (x : a)
              → pure f <*>² pure x ≡ pure (f x)
homomorphism² _ _ = refl

interchange² : ∀{a b : Set} → (u : Two (a → b)) → (y : a)
             → u <*>² pure y ≡ pure (_$ y) <*>² u
interchange² (TwoOf _ _) _ = {!!} -- looks unlawful

-- THREE (unlawful?)

infixl 5 _<*>³_

_<*>³_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b
_<*>³_ (TwoOf f _) (TwoOf x y) = TwoOf (f x) (f y)

identity³ : ∀{a : Set} → (v : Two a) → pure id <*>³ v ≡ v
identity³ (TwoOf _ _) = refl

-- FOUR (unlawful?)

infixl 5 _<*>⁴_

_<*>⁴_ : ∀{a : Set}{b : Set} → Two (a → b) → Two a → Two b
_<*>⁴_ (TwoOf _ g) (TwoOf x y) = TwoOf (g x) (g y)

identity⁴ : ∀{a : Set} → (v : Two a) → pure id <*>⁴ v ≡ v
identity⁴ (TwoOf _ _) = refl

-- ETC (unlawful?)

{- There seem to be 12 other ways to implement this that would typecheck.
-- For each of the variations above, you could:
-- 1. Only make use of x (4 more)
-- 2. Only make use of y (4 more)
-- 3. Invert the final two subexpressions (4 more)
-}