Like either but applicative instance accumulates lefts

ThisOrThese.agda

module Data.ThisOrThese where

open import Data.List.Base
open import Data.List.NonEmpty
open import Relation.Binary.PropositionalEquality.Core
open import Function

-- Apparently this is called ValidatedNel in Cats.
data ThisOrThese : Set -> Set -> Set where
  These : ∀ {A B} -> List⁺ A -> ThisOrThese A B
  This : ∀ {A B} -> B -> ThisOrThese A B

fmap : ∀{M A B} -> (A -> B) -> ThisOrThese M A -> ThisOrThese M B
fmap _ (These x) = These x
fmap f (This x) = This (f x)

functorIdentity : ∀{M A} -> (x : ThisOrThese M A) -> fmap id x ≡ x
functorIdentity (These _) = refl
functorIdentity (This _) = refl

functorComposition : ∀{M A B C}
                   -> (x : ThisOrThese M A) -> (g : A -> B) -> (f : B -> C)
                   -> fmap (f ∘ g) x ≡ fmap f (fmap g x)
functorComposition (These _) _ _ = refl
functorComposition (This _) _ _ = refl

infixl 5 _<*>_

_<*>_ : ∀{M A B} -> ThisOrThese M (A -> B) -> ThisOrThese M A -> ThisOrThese M B
These x₁ <*> These x₂ = These (x₁ ⁺++⁺ x₂)
These x <*> This _ = These x
This _ <*> These x = These x
This f <*> This x = This (f x)

pure : ∀{M A} -> A -> ThisOrThese M A
pure = This

plain∘ : ∀{A B C : Set} -> (B -> C) -> (A -> B) -> (A -> C)
plain∘ f g x = f (g x)

applicativeIdentity : ∀{M A} -> (x : ThisOrThese M A) -> pure id <*> x ≡ x
applicativeIdentity (These _) = refl
applicativeIdentity (This _) = refl

applicativeComposition : ∀ {M A B C}
                       -> (x : ThisOrThese M A)
                       -> (g : ThisOrThese M (A -> B))
                       -> (f : ThisOrThese M (B -> C))
                       -> pure plain∘ <*> f <*> g <*> x ≡ f <*> (g <*> x)
applicativeComposition (These x₁) (These x₂) (These x₃) = {!!} -- Struggling to prove this to Agda
applicativeComposition (These x₁) (These x₂) (This x₃) = refl
applicativeComposition (These x₁) (This x₂) (These x₃) = refl
applicativeComposition (These x₁) (This x₂) (This x₃) = refl
applicativeComposition (This x) (These x₁) (These x₂) = refl
applicativeComposition (This x) (These x₁) (This x₂) = refl
applicativeComposition (This x) (This x₁) (These x₂) = refl
applicativeComposition (This x) (This x₁) (This x₂) = refl

-- Agda yelling at me here; don't understand why
--applicativeHomomorphism : ∀{A B} -> (x : A) -> (f : A -> B)
--                        -> pure f <*> pure x ≡ pure (f x)
--applicativeHomomorphism x f = refl

applicativeInterchange : ∀{A B M} -> (x : A) -> (f : ThisOrThese M (A -> B))
                        -> f <*> pure x ≡ pure (λ g → g x) <*> f
applicativeInterchange x (These _) = refl
applicativeInterchange x (This _) = refl