Proper subsets

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

Created on 2022-09-12.
Last modified on 2023-06-08.

module foundation.proper-subtypes where
Imports 
open import foundation.complements-subtypes
open import foundation.inhabited-subtypes
open import foundation.universe-levels

open import foundation-core.propositions
open import foundation-core.subtypes

Idea

A subtype of a type is said to be proper if its complement is inhabited.

is-proper-subtype-Prop :
  {l1 l2 : Level} {A : UU l1} → subtype l2 A → Prop (l1 ⊔ l2)
is-proper-subtype-Prop P =
  is-inhabited-subtype-Prop (complement-subtype P)

Recent changes