Agda: Equivalence relation for sub-colists

Question

I would like to define an equality on CoList (Maybe Nat)s that only takes the justs into account. Of course, I can't just go from CoList (Maybe A) to CoList A, because that wouldn't necessarily be productive.

My question, then, is how could I define such an equivalence relation (with no eye towards decideability)? Does it help, if I can regard infinite just tails as non-equivalent?

@gallais, below, suggests I should be able to naïvely define this relation:

open import Data.Colist
open import Data.Maybe
open import Coinduction
open import Relation.Binary

module _ where
  infix 4 _∼_

  data _∼_ {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
    end : [] ∼ []
    nothingˡ : ∀ {xs ys} → ∞ (♭ xs ∼ ys) → nothing ∷ xs ∼ ys
    nothingʳ : ∀ {xs ys} → ∞ (xs ∼ ♭ ys) → xs ∼ nothing ∷ ys
    justs : ∀ {x xs ys} → ∞ (♭ xs ∼ ♭ ys) → just x ∷ xs ∼ just x ∷ ys

but proving it's transitive gets into (expected) problems from the termination checker:

  refl : ∀ {A} → Reflexive (_∼_ {A})
  refl {A} {[]} = end
  refl {A} {just x ∷ xs} = justs (♯ refl)
  refl {A} {nothing ∷ xs} = nothingˡ (♯ nothingʳ (♯ refl)) -- note how I could have defined this the other way round as well...

  drop-nothingˡ : ∀ {A xs} {ys : Colist (Maybe A)} → nothing ∷ xs ∼ ys → ♭ xs ∼ ys
  drop-nothingˡ (nothingˡ x) = ♭ x
  drop-nothingˡ (nothingʳ x) = nothingʳ (♯ drop-nothingˡ (♭ x))

  trans : ∀ {A} → Transitive (_∼_ {A})
  trans end end = end
  trans end (nothingʳ e2) = nothingʳ e2
  trans (nothingˡ e1) e2 = nothingˡ (♯ trans (♭ e1) e2)
  trans (nothingʳ e1) (nothingˡ e2) = trans (♭ e1) (♭ e2) -- This is where the problem is
  trans (nothingʳ e1) (nothingʳ e2) = nothingʳ (♯ trans (♭ e1) (drop-nothingˡ (♭ e2)))
  trans (justs e1) (nothingʳ e2) = nothingʳ (♯ trans (justs e1) (♭ e2))
  trans (justs e1) (justs e2) = justs (♯ (trans (♭ e1) (♭ e2)))

So I tried making the case where both sides are nothing less ambiguous (like how @Vitus suggested):

module _ where
  infix 4 _∼_

  data _∼_ {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
    end : [] ∼ []
    nothings : ∀ {xs ys} → ∞ (♭ xs ∼ ♭ ys) → nothing ∷ xs ∼ nothing ∷ ys
    nothingˡ : ∀ {xs y ys} → ∞ (♭ xs ∼ just y ∷ ys) → nothing ∷ xs ∼ just y ∷ ys
    nothingʳ : ∀ {x xs ys} → ∞ (just x ∷ xs ∼ ♭ ys) → just x ∷ xs ∼ nothing ∷ ys
    justs : ∀ {x xs ys} → ∞ (♭ xs ∼ ♭ ys) → just x ∷ xs ∼ just x ∷ ys

  refl : ∀ {A} → Reflexive (_∼_ {A})
  refl {A} {[]} = end
  refl {A} {just x ∷ xs} = justs (♯ refl)
  refl {A} {nothing ∷ xs} = nothings (♯ refl)

  sym : ∀ {A} → Symmetric (_∼_ {A})
  sym end = end
  sym (nothings xs∼ys) = nothings (♯ sym (♭ xs∼ys))
  sym (nothingˡ xs∼ys) = nothingʳ (♯ sym (♭ xs∼ys))
  sym (nothingʳ xs∼ys) = nothingˡ (♯ sym (♭ xs∼ys))
  sym (justs xs∼ys) = justs (♯ sym (♭ xs∼ys))

  trans : ∀ {A} → Transitive (_∼_ {A})
  trans end ys∼zs = ys∼zs
  trans (nothings xs∼ys) (nothings ys∼zs) = nothings (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothings xs∼ys) (nothingˡ ys∼zs) = nothingˡ (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothingˡ xs∼ys) (nothingʳ ys∼zs) = nothings (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans (nothingˡ xs∼ys) (justs ys∼zs) = nothingˡ (♯ trans (♭ xs∼ys) (justs ys∼zs))
  trans (nothingʳ xs∼ys) (nothings ys∼zs) = nothingʳ (♯ trans (♭ xs∼ys) (♭ ys∼zs))
  trans {A} {just x ∷ xs} {nothing ∷ ys} {just z ∷ zs} (nothingʳ xs∼ys) (nothingˡ ys∼zs) = ?
  trans (justs xs∼ys) (nothingʳ ys∼zs) = nothingʳ (♯ trans (justs xs∼ys) (♭ ys∼zs))
  trans (justs xs∼ys) (justs ys∼zs) = justs (♯ trans (♭ xs∼ys) (♭ ys∼zs))

but now I don't know how to define the problematic case of trans (the one where I left a hole)

Answer 1

After much deliberation and spam in the comments section of the question (and procrastinating updating my local Agda to a version that has a real termination checker), I came up with this:

module Subcolist where

open import Data.Colist
open import Data.Maybe
open import Coinduction
open import Relation.Binary

module _ {a} {A : Set a} where
  infix 4 _∼_

  data _∼_ : Colist (Maybe A) → Colist (Maybe A) → Set a where
    end      : [] ∼ []
    nothings : ∀ {  xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → nothing ∷ xs ∼ nothing ∷ ys
    nothingˡ : ∀ {  xs ys} (r :   (♭ xs ∼   ys)) → nothing ∷ xs ∼           ys
    nothingʳ : ∀ {  xs ys} (r :   (  xs ∼ ♭ ys)) →           xs ∼ nothing ∷ ys
    justs    : ∀ {x xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → just x  ∷ xs ∼ just x  ∷ ys


  refl : Reflexive _∼_
  refl {[]} = end
  refl {just x ∷ xs} = justs (♯ refl)
  refl {nothing ∷ xs} = nothings (♯ refl)

  sym : Symmetric _∼_
  sym end = end
  sym (nothings xs∼ys) = nothings (♯ sym (♭ xs∼ys))
  sym (nothingˡ xs∼ys) = nothingʳ   (sym   xs∼ys)
  sym (nothingʳ xs∼ys) = nothingˡ   (sym   xs∼ys)
  sym (justs    xs∼ys) = justs    (♯ sym (♭ xs∼ys))

  drop-nothingˡ : ∀ {xs} {ys : Colist (Maybe A)} → nothing ∷ xs ∼ ys → ♭ xs ∼ ys
  drop-nothingˡ (nothings r) = nothingʳ (♭ r)
  drop-nothingˡ (nothingˡ r) = r
  drop-nothingˡ (nothingʳ r) = nothingʳ (drop-nothingˡ r)

  drop-nothingʳ : ∀ {xs : Colist (Maybe A)} {ys} → xs ∼ nothing ∷ ys → xs ∼ ♭ ys
  drop-nothingʳ (nothings r) = nothingˡ (♭ r)
  drop-nothingʳ (nothingˡ r) = nothingˡ (drop-nothingʳ r)
  drop-nothingʳ (nothingʳ r) = r

  drop-nothings : ∀ {xs ys : ∞ (Colist (Maybe A))} → nothing ∷ xs ∼ nothing ∷ ys → ♭ xs ∼ ♭ ys
  drop-nothings (nothings r) = ♭ r
  drop-nothings (nothingˡ r) = drop-nothingʳ r
  drop-nothings (nothingʳ r) = drop-nothingˡ r

  []-trans : ∀ {xs ys : Colist (Maybe A)} → xs ∼ ys → ys ∼ [] → xs ∼ []
  []-trans xs∼ys end = xs∼ys
  []-trans xs∼ys (nothingˡ ys∼[]) = []-trans (drop-nothingʳ xs∼ys) ys∼[]

  mutual    
    just-trans : ∀ {xs ys zs} {z : A} → xs ∼ ys → ys ∼ just z ∷ zs → xs ∼ just z ∷ zs
    just-trans (justs r) (justs r₁) = justs (♯ (trans (♭ r) (♭ r₁)))
    just-trans (nothingˡ xs∼ys) ys∼zs = nothingˡ (just-trans xs∼ys ys∼zs)
    just-trans xs∼ys (nothingˡ ys∼zs) = just-trans (drop-nothingʳ xs∼ys) ys∼zs

    nothing-trans : ∀ {xs ys : Colist (Maybe A)} {zs} → xs ∼ ys → ys ∼ nothing ∷ zs → xs ∼ nothing ∷ zs
    nothing-trans (nothings xs∼ys) ys∼zs = nothings (♯ trans (♭ xs∼ys) (drop-nothings ys∼zs))
    nothing-trans (nothingˡ xs∼ys) ys∼zs = nothings (♯ (trans xs∼ys (drop-nothingʳ ys∼zs)))
    nothing-trans (nothingʳ xs∼ys) ys∼zs = nothing-trans xs∼ys (drop-nothingˡ ys∼zs)
    nothing-trans {xs = just x  ∷ xs} xs∼ys (nothingʳ ys∼zs) = nothingʳ (trans xs∼ys ys∼zs)
    nothing-trans end xs∼ys = xs∼ys

    trans : Transitive _∼_
    trans {k = []}           xs∼ys ys∼zs = []-trans      xs∼ys ys∼zs
    trans {k = nothing ∷ ks} xs∼ys ys∼zs = nothing-trans xs∼ys ys∼zs
    trans {k = just k  ∷ ks} xs∼ys ys∼zs = just-trans    xs∼ys ys∼zs

  equivalence : Setoid a a
  equivalence = record 
    { _≈_ = _∼_
    ; isEquivalence = record 
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    }

I use mixed induction-coinduction and I believe it captures the notion you want. I needed to jump through some hoops to get past the termination/productivity checker as the naive version of trans does not pass it, but this seems to work. It was inspired in part by something I learned from Nils Anders Danielsson's implementation of the partiality monad, which has a similar sort of relation definition in there. It's not as complicated as this one, but the work to get Agda to accept it is largely similar. To generalize it slightly, it would seem more friendly to treat this as a setoid transformer and not just assume definitional/propositional equality for the justs case but that's a trivial change.

I did notice that the other two proposals outlaw nothing ∷ nothing ∷ [] ∼ [] which seemed contrary to the original question, so I edited the type to support that again. I think doing so stopped _∼_ from being uniquely inhabited, but fixing that would probably lead to several more constructors in the relation type and that was more effort than seemed worthwhile.

It's worth noting that at the time I'm writing this, Agda has an open bug (#787) in its termination checker that applies to my version. I'm not sure what causes that bug so I can't guarantee my version is entirely sound, but it makes sense to me.

Answer 2

Just to try a different approach, I've decided to go with a data type for the list semantics:

data Sem (A : Set) : Set where
  [] : Sem A
  ⊥ : Sem A
  _∷_ : A → ∞ (Sem A) → Sem A

together with an undecidable binary relation between lists and their semantics:

data _HasSem_ {A : Set} : Colist (Maybe A) → Sem A → Set where
  [] : [] HasSem []
  ⊥ : ∀ {l} → ∞ (♭ l HasSem ⊥) → (nothing ∷ l) HasSem ⊥
  n∷_ : ∀ {l s} → ♭ l HasSem s → (nothing ∷ l) HasSem s
  _∷_ : ∀ {l s} x → ∞ (♭ l HasSem ♭ s) → (just x ∷ l) HasSem (x ∷ s)

Then the definition of list equality up to semantics is easy:

a ≈ b = ∀ s → a HasSem s → b HasSem s

isEquivalence is mostly trivial then, except for sym, where it looks like you need to make that arrow bidirectional (a HasSem s ⇔ b HasSem s) to prove that constructively.

I then tried to prove my notion of equality equivalent to copumpkin's, where I had some trouble. I was able to prove one direction constructively:

from : ∀ {a b} → a ∼ b → a ≈ b

However, I was only able to go the other direction after postulating Excluded Middle:

LEM = (A : Set) → Dec A
to : LEM → ∀ {a b} → a ≈ b → a ∼ b

I wasn't able to prove a nicer non-constructive version of to either:

nicer-to : ∀ {a b} → a ≈ b → ¬ ¬ a ∼ b -- Not proven

The full code follows. There are proofs for some other properties too, for example the proof of existence and uniqueness of semantics, assuming LEM.

module colists where

open import Coinduction
open import Data.Colist hiding (_≈_)

data Sem (A : Set) : Set where
  [] : Sem A
  ⊥ : Sem A
  _∷_ : A → ∞ (Sem A) → Sem A

open import Data.Maybe

data _HasSem_ {A : Set} : Colist (Maybe A) → Sem A → Set where
  [] : [] HasSem []
  ⊥ : ∀ {l} → ∞ (♭ l HasSem ⊥) → (nothing ∷ l) HasSem ⊥
  n∷_ : ∀ {l s} → ♭ l HasSem s → (nothing ∷ l) HasSem s
  _∷_ : ∀ {l s} x → ∞ (♭ l HasSem ♭ s) → (just x ∷ l) HasSem (x ∷ s)

open import Function.Equivalence

_≈_ : ∀ {A : Set} → Colist (Maybe A) → Colist (Maybe A) → Set
a ≈ b = ∀ s → a HasSem s → b HasSem s

data _∼_  {A : Set} : Colist (Maybe A) → Colist (Maybe A) → Set where
    end      : [] ∼ []
    nothings : ∀ {  xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → (nothing ∷ xs) ∼ (nothing ∷ ys)
    nothingˡ : ∀ {  xs ys} (r :   (♭ xs ∼   ys)) → (nothing ∷ xs) ∼           ys
    nothingʳ : ∀ {  xs ys} (r :   (  xs ∼ ♭ ys)) →           xs ∼ (nothing ∷ ys)
    justs    : ∀ {x xs ys} (r : ∞ (♭ xs ∼ ♭ ys)) → (just x  ∷ xs) ∼ (just x  ∷ ys)

module WithA (A : Set) where

  CLMA = Colist (Maybe A)

  from-[] : ∀ {a b : CLMA} → a ∼ b → a HasSem [] → b HasSem []
  from-[] end [] = []
  from-[] (nothingʳ r) a-has = n∷ (from-[] r a-has)
  from-[] (nothings r) (n∷ y) = n∷ (from-[] (♭ r) y)
  from-[] (nothingˡ r) (n∷ y) = from-[] r y
  from-[] (justs _) ()

  from-⊥ : ∀ {a b : CLMA} → a ∼ b → a HasSem ⊥ → b HasSem ⊥
  from-⊥ (nothings r) (⊥ y) = ⊥ (♯ (from-⊥ (♭ r) (♭ y)))
  from-⊥ (nothingˡ r) (⊥ y) = from-⊥ r (♭ y)
  from-⊥ (nothingʳ r) (⊥ y) = ⊥ (♯ (from-⊥ r (⊥ y)))
  from-⊥ (nothings r) (n∷ y) = ⊥ (♯ (from-⊥ (♭ r) y))
  from-⊥ (nothingˡ r) (n∷ y) = from-⊥ r y
  from-⊥ (nothingʳ r) (n∷ y) = ⊥ (♯ (from-⊥ r (⊥ (♯ y))))
  from-⊥ (justs _) ()
  from-⊥ end ()

  from' : ∀ {a b : CLMA} {s} → a ∼ b → a HasSem s → b HasSem s
  from-∷ : ∀ {a b : CLMA} {x s} → a ∼ b → a HasSem (x ∷ s) → b HasSem (x ∷ s)
  from' {a} {b} {[]} eq sem = from-[] eq sem
  from' {a} {b} {⊥} eq sem = from-⊥ eq sem
  from' {a} {b} {y ∷ y'} eq sem = from-∷ eq sem

  from-∷ (nothings r) (n∷ y) = n∷ from-∷ (♭ r) y
  from-∷ (nothingˡ r) (n∷ y) = from-∷ r y
  from-∷ (nothingʳ r) (n∷ y) = n∷ from-∷ r (n∷ y)
  from-∷ (nothingʳ r) (x ∷ y) = n∷ (from-∷ r (x ∷ y))
  from-∷ (justs r) (x ∷ y) = x ∷ ♯ from' (♭ r) (♭ y)
  from-∷ end ()

  from : ∀ {a b : CLMA} → a ∼ b → a ≈ b
  from eq sem has = from' eq has

  refl : ∀ (a : CLMA) → a ≈ a
  refl a = λ s z → z

  trans : ∀ (a b c : CLMA) → a ≈ b → b ≈ c → a ≈ c
  trans a b c ab bc s as = bc s (ab s as)

  open import Relation.Nullary
  open import Data.Product

  data AllNothing : CLMA → Set where
   allNothing : ∀ {l} → ∞ (AllNothing (♭ l)) → AllNothing (nothing ∷ l)
   [] : AllNothing []

  data HasJust : CLMA → Set where
   just : ∀ x l → HasJust (just x ∷ l)
   nothing : ∀ l → HasJust (♭ l) → HasJust (nothing ∷ l)

  import Data.Empty

  notSomeMeansAll : ∀ {x} → ¬ HasJust x → AllNothing x
  notSomeMeansAll {[]} ns = []
  notSomeMeansAll {just x ∷ xs} ns with ns (just x xs)
  ... | ()
  notSomeMeansAll {nothing ∷ xs} ns = allNothing {xs} ( ♯ notSomeMeansAll {♭ xs} (λ z → ns (nothing xs z)) )

  data HasBot : CLMA → Set where
    ⊥ : ∀ l → ∞ (HasBot (♭ l)) → HasBot (nothing ∷ l)
    _∷_ : ∀ x l → HasBot (♭ l) → HasBot (x ∷ l)

  data IsBot : CLMA → Set where
    ⊥ : ∀ {l} → ∞ (IsBot (♭ l)) → IsBot (nothing ∷ l)

  data IsEmpty : CLMA → Set where
    [] : IsEmpty []
    n∷_ : ∀ {l} → IsEmpty (♭ l) → IsEmpty (nothing ∷ l)

  getAfterJust : {a : CLMA} → HasJust a → A × CLMA
  getAfterJust (just x l) = x , ♭ l
  getAfterJust (nothing l y) = getAfterJust y

  data SemStream : Colist (Maybe A) → Set where
    [] : ∀ {l} → IsEmpty l → SemStream l
    ⊥ : ∀ {l} → IsBot l → SemStream l
    _∷_ : ∀ {l} → (hj : HasJust l) → ∞ (SemStream (proj₂ (getAfterJust hj))) → SemStream l

  getSem : ∀ {a} → SemStream a → Sem A
  go : ∀ {a} → SemStream a → ∞ (Sem A)
  go rec = ♯ getSem rec
  getSem ([] _) = []
  getSem (⊥ _) = ⊥
  getSem {a} (hj ∷ rec) = proj₁ (getAfterJust hj) ∷ go (♭ rec)

  getSem-empty-good : ∀ {a} → IsEmpty a → a HasSem []
  getSem-empty-good [] = []
  getSem-empty-good (n∷ y) = n∷ getSem-empty-good y

  getSem-good : ∀ {a} (s : SemStream a) → a HasSem getSem s
  getSem-good ([] emp) = getSem-empty-good emp
  getSem-good (⊥ (⊥ y)) = ⊥ (♯ getSem-good (⊥ (♭ y)))
  getSem-good (just x l ∷ y) = x ∷ (♯ getSem-good (♭ y))
  getSem-good (nothing l y ∷ y') = n∷ getSem-good (y ∷ y')

  allNothing-variants' : ∀ {a} → ¬ IsEmpty a → AllNothing a → IsBot a
  allNothing-variants' nie (allNothing y) = ⊥ (♯  allNothing-variants' (λ z → nie (n∷ z)) (♭ y))
  allNothing-variants' nie [] with nie []
  ... | ()

  open import Data.Sum

  module WithEM (EM : (A : Set) → Dec A) where

    allNothing-variants : ∀ {a} → AllNothing a → IsEmpty a ⊎ IsBot a
    allNothing-variants {a} an with EM (IsEmpty a)
    ... | yes ie = inj₁ ie
    ... | no nie = inj₂ (allNothing-variants' nie an)

    mustbe : ∀ (a : CLMA) → SemStream a
    mustbe a with EM (HasJust a)
    mustbe a | yes p = p ∷ (♯ mustbe _)
    mustbe a | no ¬p with notSomeMeansAll ¬p
    ... | all with allNothing-variants all
    ... | inj₁ x = [] x
    ... | inj₂ y = ⊥ y

    mustbe' : ∀ (a : CLMA) → ∃ (λ s → a HasSem s)
    mustbe' a = getSem (mustbe a) , getSem-good (mustbe a)

    data Sem-Eq : Sem A → Sem A → Set where
      [] : Sem-Eq [] []
      ⊥ : Sem-Eq ⊥ ⊥
      _∷_ : ∀ x {a b} → ∞ (Sem-Eq (♭ a) (♭ b)) → Sem-Eq (x ∷ a) (x ∷ b)

    sem-unique⊥ : ∀ {x b} → x HasSem ⊥ → x HasSem b → Sem-Eq ⊥ b
    sem-unique⊥ () []
    sem-unique⊥ s⊥ (⊥ y) = ⊥
    sem-unique⊥ (⊥ y) (n∷ y') = sem-unique⊥ (♭ y) y'
    sem-unique⊥ (n∷ y) (n∷ y') = sem-unique⊥ y y'

    sem-unique' : ∀ {x a b} → x HasSem a → x HasSem b → Sem-Eq a b
    sem-unique' [] [] = []
    sem-unique' (⊥ y) hasb = sem-unique⊥ (⊥ y) hasb
    sem-unique' (n∷ y) (⊥ y') = sem-unique' y (♭ y')
    sem-unique' (n∷ y) (n∷ y') = sem-unique' y y'
    sem-unique' (x ∷ y) (.x ∷ y') = x ∷ (♯ sem-unique' (♭ y) (♭ y'))

    to' : ∀ {a b : Colist (Maybe A)} {s} → a HasSem s → b HasSem s → a ∼ b
    to' [] [] = end
    to' [] (n∷ y) = nothingʳ (to' [] y)
    to' (⊥ y) (⊥ y') = nothings (♯ to' (♭ y) (♭ y'))
    to' (⊥ y) (n∷ y') = nothings (♯ to' (♭ y) y')
    to' (n∷ y) [] = nothingˡ (to' y [])
    to' (n∷ y) (⊥ y') = nothings (♯ to' y (♭ y'))
    to' (n∷ y) (n∷ y') = nothings (♯ to' y y')
    to' (n∷ y) (x ∷ y') = nothingˡ (to' y (x ∷ y'))
    to' (x ∷ y) (n∷ y') = nothingʳ (to' (x ∷ y) y')
    to' (x ∷ y) (.x ∷ y') = justs (♯ to' (♭ y) (♭ y'))

    to : ∀ (a b : Colist (Maybe A)) → a ≈ b → a ∼ b
    to a b eq with mustbe' a
    ... | s , a-s with eq s a-s
    ... | b-s = to' a-s b-s

    hasSem-respects : ∀ {x s1 s2} → x HasSem s1 → Sem-Eq s1 s2 → x HasSem s2
    hasSem-respects [] [] = []
    hasSem-respects (⊥ y) ⊥ = ⊥ y
    hasSem-respects (n∷ y) eq = n∷ hasSem-respects y eq
    hasSem-respects (x ∷ y) (.x ∷ y') = x ∷ ♯ hasSem-respects (♭ y) (♭ y')

    sym' : ∀ (a b : CLMA) → a ≈ b → b ≈ a
    sym' a b eq s b-s with mustbe' a
    ... | s' , a-s' = hasSem-respects a-s' (sem-unique' (eq s' a-s') b-s)

Answer 3

Just write down what you want as a coinductive relation!

module colist where

open import Coinduction
open import Data.Maybe

data CoList (A : Set) : Set where
  ■ : CoList A
  _∷_ : A → ∞ (CoList A) → CoList A

data EqCoList {A : Set} : CoList (Maybe A) → CoList (Maybe A) → Set where
-- two empty lists are equal
  conil : EqCoList ■ ■
-- nothings do not matter equality-wise
  nonel : ∀ xs ys → ∞ (EqCoList (♭ xs) ys) → EqCoList (nothing ∷ xs) ys
  noner : ∀ xs ys → ∞ (EqCoList xs (♭ ys)) → EqCoList xs (nothing ∷ ys)
-- justs have to agree
  justs : ∀ x xs ys → ∞ (EqCoList (♭ xs) (♭ ys)) → EqCoList (just x ∷ xs) (just x ∷ ys)