{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness #-}

module Agda.Builtin.Cubical.Sub where

  open import Agda.Primitive.Cubical

  {-# BUILTIN SUB Sub #-}

  postulate
    inS :  {} {A : Set } {φ} (x : A)  Sub A φ  _  x)

  {-# BUILTIN SUBIN inS #-}

  -- Sub A φ u is treated as A.
  {-# COMPILE JS inS = _ => _ => _ => x => x #-}

  primitive
    primSubOut :  {} {A : Set } {φ : I} {u : Partial φ A}  Sub _ φ u  A