⚠️ 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-compatible --safe --no-sized-types --no-guardedness --level-universe #-} module Agda.Builtin.Strict where open import Agda.Builtin.Equality primitive primForce : ∀ {a b } {A : Set a } {B : A → Set b } (x : A ) → (∀ x → B x ) → B x primForceLemma : ∀ {a b } {A : Set a } {B : A → Set b } (x : A ) (f : ∀ x → B x ) → primForce x f ≡ f x