{-# OPTIONS --without-K --safe #-} module Layered.Typ where open import Data.List open import Lib hiding (lookup) public infixr 5 _⟶_ -- types data Typ : Set where N : Typ _⟶_ : Typ → Typ → Typ □ : Typ → Typ Ctx : Set Ctx = List Typ variable S T U : Typ Γ Γ′ Γ″ : Ctx Δ Δ′ Δ″ : Ctx Ψ Ψ′ Ψ″ : Ctx Φ Φ′ Φ″ : Ctx -- Layering predicates ---------------------- data core? : Typ → Set where N : core? N _⟶_ : core? S → core? T → core? (S ⟶ T) data type? : Typ → Set where N : type? N _⟶_ : type? S → type? T → type? (S ⟶ T) □ : core? T → type? (□ T) cores? : Ctx → Set cores? = All core? types? : Ctx → Set types? = All type? core-type : core? T → type? T core-type N = N core-type (S ⟶ T) = core-type S ⟶ core-type T cores-types : cores? Ψ → types? Ψ cores-types = All′.map core-type