```------------------------------------------------------------------------
-- A type for values that should be erased at run-time
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies
-- (in particular, not Function-universe) that do not rely on
-- equality. See Erased and other modules under Erased for more
-- definitions. The definitions below are reexported from
-- Erased.Level-1.

{-# OPTIONS --cubical-compatible --safe #-}

module Erased.Basics where

open import Prelude

private
variable
a p q : Level

-- Erased A is like A, but the values are (supposed to be) erased at
-- run-time.

record Erased (@0 A : Type a) : Type a where
constructor [_]
field
@0 erased : A

open Erased public

-- A variant of [_] that does not take an erased argument.

[_]→ : {@0 A : Type a} → A → Erased A
[ x ]→ = [ x ]

-- A variant of [_]→.

[_∣_]→ : (@0 A : Type a) → A → Erased A
[_∣_]→ _ = [_]→

-- A type A is stable if Erased A implies A.

Stable : Type a → Type a
Stable A = Erased A → A

-- Erased preserves dependent functions.

map :
{@0 A : Type a} {@0 P : A → Type p} →
@0 ((x : A) → P x) → (x : Erased A) → Erased (P (erased x))
map f [ x ] = [ f x ]

-- A binary variant of map.

zip :
{@0 A : Type a} {@0 P : A → Type p} {@0 Q : {x : A} → P x → Type q} →
@0 ((x : A) (p : P x) → Q p) →
(([ x ]) : Erased A) (([ p ]) : Erased (P x)) → Erased (Q p)
zip f [ x ] [ p ] = [ f x p ]
```