Unique existence

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Elisabeth Bonnevier.

Created on 2022-06-02.
Last modified on 2023-06-08.

module foundation.unique-existence where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-types

Idea

Unique existence ∃! A B is defined as Σ A B being contractible.

Definition

∃! : {l1 l2 : Level} → (A : UU l1) → (A → UU l2) → UU (l1 ⊔ l2)
∃! A B = is-contr (Σ A B)

Recent changes