⚠️ Archived site. This is the pre-3.0 Agda Universal Algebra Library, preserved for reference. Its current home is agda-algebras.universalalgebra.org (as of July 2026).

{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness --no-subtyping #-} module Agda.Builtin.Cubical.Sub where open import Agda.Primitive.Cubical {-# BUILTIN SUB Sub #-} postulate inc : ∀ {ℓ } {A : Set ℓ } {φ } (x : A ) → Sub A φ (λ _ → x ) {-# BUILTIN SUBIN inc #-} primitive primSubOut : ∀ {ℓ } {A : Set ℓ } {φ : I } {u : Partial φ A } → Sub _ φ u → A