Closure, for the third time

Third.agda

open import Agda.Builtin.Sigma

open import Decidable
open import List

module Third (Ω : Set) (_≟_ : Decidable≡ Ω) where

data Filter {A : Set} (P : Pred A) : List A → List A → Set where
  []   : Filter P [] []
  _∷_  : ∀{x xs ys} → P x    → Filter P xs ys → Filter P (x ∷ xs) (x ∷ ys)
  _-∷_ : ∀{x xs ys} → ¬(P x) → Filter P xs ys → Filter P (x ∷ xs) ys

filter : {A : Set} {P : Pred A} → (p : Decidable P) → (xs : List A) → Σ (List A) (Filter P xs)
filter p [] = [] , []
filter p (x ∷ xs) with p x | filter p xs
filter p (x ∷ xs) | yes x₁ | fst₁ , snd₁ = x ∷ fst₁ , (x₁ ∷ snd₁)
filter p (x ∷ xs) | no x₁ | fst₁ , snd₁ = fst₁ , (x₁ -∷ snd₁)

data Arrow : Set where
  _⇒_ : (α β : Ω) → Arrow

postulate arrowEq : Decidable≡ Arrow

data _IsPremiseOf_ (α : Ω) : Arrow → Set where
  left : ∀ β → α IsPremiseOf (α ⇒ β)

postulate _isPremiseOf_ : (α : Ω) → (r : Arrow) → Dec (α IsPremiseOf r)


data PathUnder_From_To_ (Δ : List Arrow) (α : Ω) : Ω → Set where
  ε   : PathUnder Δ From α To α
  _>_ : ∀{β γ} → PathUnder Δ From α To β → (β ⇒ γ) ∈ Δ → PathUnder Δ From α To γ

record ClosureOf_Under_Is_ (Γ : List Ω) (Δ : List Arrow) (Φ : List Ω) : Set where
  constructor mkclosure
  field
    reach : ∀ β → β ∈ Φ → Σ Ω (λ α → Σ (α ∈ Γ) λ _ → PathUnder Δ From α To β)
    base : ∀ α → α ∈ Γ → α ∈ Φ
    step : ∀ α β → α ∈ Φ → (α ⇒ β) ∈ Δ → β ∈ Φ

closure : (Γ : List Ω) → (Δ : List Arrow) → Σ (List Ω) ClosureOf Γ Under Δ Is_
closure [] Δ = [] , mkclosure (λ β ()) (λ α z → z) (λ α β ())
closure (α ∷ Γ) Δ with filter (α isPremiseOf_) Δ
closure (α ∷ Γ) Δ | fst₁ , snd₁ = {!   !}