module Zipper where import Derivative import Functor import Sets open Functor open Derivative open Semantics open Recursive open Sets Zipper : U -> Set Zipper F = List (⟦ ∂ F ⟧ (μ F)) -- Plugging a zipper unzip : {F : U} -> Zipper F -> μ F -> μ F unzip [] t = t unzip {F} (c :: γ) t = inn (plug-∂ F c (unzip γ t))
