{-# OPTIONS --without-K --safe #-} module CLayered.Typ where open import Data.List open import Lib hiding (lookup) public infixr 5 _⟶_ mutual -- types data Typ : Set where N : Typ _⟶_ : Typ → Typ → Typ □ : LCtx → Typ → Typ LCtx : Set LCtx = List Typ GCtx : Set GCtx = List (LCtx × Typ) variable S T U : Typ S′ T′ U′ : Typ Γ Γ′ Γ″ : LCtx Δ Δ′ Δ″ : LCtx Ψ Ψ′ Ψ″ : GCtx Φ Φ′ Φ″ : GCtx data Layer : Set where zer one : Layer variable i : Layer -- Layering predicates ---------------------- mutual data wf? : Layer → Typ → Set where N : wf? i N _⟶_ : wf? i S → wf? i T → wf? i (S ⟶ T) □ : wfs? zer Γ → wf? zer T → wf? one (□ Γ T) wfs? : Layer → LCtx → Set wfs? i Γ = All (wf? i) Γ gwf? : LCtx × Typ → Set gwf? (Γ , T) = wfs? zer Γ × wf? zer T gwfs? : GCtx → Set gwfs? Ψ = All gwf? Ψ core? : Typ → Set core? = wf? zer type? : Typ → Set type? = wf? one cores? : LCtx → Set cores? = wfs? zer types? : LCtx → Set types? = wfs? one wf-lift : core? T → type? T wf-lift N = N wf-lift (S ⟶ T) = wf-lift S ⟶ wf-lift T wfs-lift : cores? Γ → types? Γ wfs-lift = All′.map wf-lift wf-lift′ : wf? zer T → wf? i T wf-lift′ N = N wf-lift′ (S ⟶ T) = wf-lift′ S ⟶ wf-lift′ T wfs-lift′ : wfs? zer Γ → wfs? i Γ wfs-lift′ = All′.map wf-lift′