Agda - coinductive colist relation

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
infixr 2 _j₂_

data _j₂_ {A : Set} : CoList (Maybe A)  CoList (Maybe A)  Set where
  nil   :                                                           [] j₂           []
  noneb :  {xs ys}     (        xs j₂         ys)  nothing  xs j₂ nothing  ys
  nonel :  {x xs ys}   (        xs j₂ just x  ys)  nothing  xs j₂  just x  ys
  noner :  {x xs ys}   (just x  xs j₂         ys)   just x  xs j₂ nothing  ys
  justs :  {x xs ys}   (        xs j₂         ys)   just x  xs j₂  just x  ys

j₂-trans :  {A} {xs ys zs : CoList (Maybe A)}  xs j₂ ys  ys j₂ zs  xs j₂ zs
j₂-trans nil        nil       = nil
j₂-trans (noneb t₁) (noneb t₂) = noneb ( j₂-trans ( t₁) ( t₂))
j₂-trans (noneb t₁) (nonel t₂) = nonel ( j₂-trans ( t₁) ( t₂))
j₂-trans (nonel t₁) (noner t₂) = noneb ( j₂-trans ( t₁) ( t₂))
j₂-trans (nonel t₁) (justs t₂) = nonel ( j₂-trans ( t₁) (justs t₂))
j₂-trans (noner t₁) (noneb t₂) = noner ( j₂-trans ( t₁) ( t₂))
j₂-trans (noner t₁) (nonel t₃) = {!!}
j₂-trans (justs t₁) (noner t₂) = noner ( j₂-trans (justs t₁) ( t₂))
j₂-trans (justs t₁) (justs t₂) = justs ( j₂-trans ( t₁) ( t₂))

{-
Goal: just .x ∷ .xs ≈j₂ just .x₁ ∷ .ys₁
————————————————————————————————————————————————————————————
t₂   : ∞ (♭ .ys ≈j₂ just .x₁ ∷ .ys₁)
.ys₁ : ∞ (CoList (Maybe .A))
.x₁  : .A
t₁   : ∞ (just .x ∷ .xs ≈j₂ ♭ .ys)
.ys  : ∞ (CoList (Maybe .A))
.xs  : ∞ (CoList (Maybe .A))
.x   : .A
.A   : Set
-}