Unique existence

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Elisabeth Stenholm.

Created on 2022-06-02.
Last modified on 2023-11-24.

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

open import foundation-core.torsorial-type-families

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-torsorial B

Recent changes