module Implicit.Language.Counter2Mask where open import Implicit.Language.Base data Counter : Set where Z : Counter β : Counter π : Counter β Counter π : Counter β Counter c2m : Counter β Mask c2m Z = ` β c2m β = ` β‘ c2m (π j) = β‘ Β· c2m j c2m (π j) = β Β· c2m j m2c : Mask β Counter m2c (` β‘) = β m2c (` β ) = Z m2c (β‘ Β· m) = π (m2c m) m2c (β Β· m) = π (m2c m) iso1 : β j β c2m (m2c j) β‘ j iso1 (` β‘) = refl iso1 (` β ) = refl iso1 (β‘ Β· j) = congβ _Β·_ refl (iso1 j) iso1 (β Β· j) = congβ _Β·_ refl (iso1 j) iso2 : β j β m2c (c2m j) β‘ j iso2 Z = refl iso2 β = refl iso2 (π j) = cong π (iso2 j) iso2 (π j) = cong π (iso2 j)