Inhabited subtypes

module foundation.inhabited-subtypes where
Imports
open import foundation.inhabited-types
open import foundation.propositional-truncations
open import foundation.subtypes

open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.subtype-identity-principle
open import foundation-core.universe-levels

Idea

An inhabited subtype of a type A is a subtype P of A such that the underlying type of P is inhabited.

is-inhabited-subtype-Prop :
  {l1 l2 : Level} {A : UU l1}  subtype l2 A  Prop (l1  l2)
is-inhabited-subtype-Prop P = is-inhabited-Prop (type-subtype P)

is-inhabited-subtype :
  {l1 l2 : Level} {A : UU l1}  subtype l2 A  UU (l1  l2)
is-inhabited-subtype P = type-Prop (is-inhabited-subtype-Prop P)

inhabited-subtype :
  {l1 : Level} (l2 : Level)  UU l1  UU (l1  lsuc l2)
inhabited-subtype l2 A = type-subtype (is-inhabited-subtype-Prop {l2 = l2} {A})

module _
  {l1 l2 : Level} {A : UU l1} (P : inhabited-subtype l2 A)
  where

  subtype-inhabited-subtype : subtype l2 A
  subtype-inhabited-subtype = pr1 P

  is-inhabited-subtype-inhabited-subtype :
    is-inhabited-subtype subtype-inhabited-subtype
  is-inhabited-subtype-inhabited-subtype = pr2 P

  type-inhabited-subtype : UU (l1  l2)
  type-inhabited-subtype = type-subtype subtype-inhabited-subtype

  inhabited-type-inhabited-subtype : Inhabited-Type (l1  l2)
  pr1 inhabited-type-inhabited-subtype = type-inhabited-subtype
  pr2 inhabited-type-inhabited-subtype =
    is-inhabited-subtype-inhabited-subtype

  is-in-inhabited-subtype : A  UU l2
  is-in-inhabited-subtype = is-in-subtype subtype-inhabited-subtype

  is-prop-is-in-inhabited-subtype :
    (x : A)  is-prop (is-in-inhabited-subtype x)
  is-prop-is-in-inhabited-subtype =
    is-prop-is-in-subtype subtype-inhabited-subtype

  inclusion-inhabited-subtype : type-inhabited-subtype  A
  inclusion-inhabited-subtype = inclusion-subtype subtype-inhabited-subtype

  ap-inclusion-inhabited-subtype :
    (x y : type-inhabited-subtype) 
    x  y  (inclusion-inhabited-subtype x  inclusion-inhabited-subtype y)
  ap-inclusion-inhabited-subtype =
    ap-inclusion-subtype subtype-inhabited-subtype

  is-in-inhabited-subtype-inclusion-inhabited-subtype :
    (x : type-inhabited-subtype) 
    is-in-inhabited-subtype (inclusion-inhabited-subtype x)
  is-in-inhabited-subtype-inclusion-inhabited-subtype =
    is-in-subtype-inclusion-subtype subtype-inhabited-subtype

Properties

Characterization of equality of inhabited subtypes

has-same-elements-inhabited-subtype-Prop :
  {l1 l2 l3 : Level} {A : UU l1} 
  inhabited-subtype l2 A  inhabited-subtype l3 A  Prop (l1  l2  l3)
has-same-elements-inhabited-subtype-Prop P Q =
  has-same-elements-subtype-Prop
    ( subtype-inhabited-subtype P)
    ( subtype-inhabited-subtype Q)

has-same-elements-inhabited-subtype :
  {l1 l2 l3 : Level} {A : UU l1} 
  inhabited-subtype l2 A  inhabited-subtype l3 A  UU (l1  l2  l3)
has-same-elements-inhabited-subtype P Q =
  type-Prop (has-same-elements-inhabited-subtype-Prop P Q)

is-prop-has-same-elements-inhabited-subtype :
  {l1 l2 l3 : Level} {A : UU l1} 
  (P : inhabited-subtype l2 A) (Q : inhabited-subtype l3 A) 
  is-prop (has-same-elements-inhabited-subtype P Q)
is-prop-has-same-elements-inhabited-subtype P Q =
  is-prop-type-Prop (has-same-elements-inhabited-subtype-Prop P Q)

module _
  {l1 l2 : Level} {A : UU l1} (P : inhabited-subtype l2 A)
  where

  refl-has-same-elements-inhabited-subtype :
    has-same-elements-inhabited-subtype P P
  pr1 (refl-has-same-elements-inhabited-subtype x) = id
  pr2 (refl-has-same-elements-inhabited-subtype x) = id

  is-contr-total-has-same-elements-inhabited-subtype :
    is-contr
      ( Σ (inhabited-subtype l2 A) (has-same-elements-inhabited-subtype P))
  is-contr-total-has-same-elements-inhabited-subtype =
    is-contr-total-Eq-subtype
      ( is-contr-total-has-same-elements-subtype
        ( subtype-inhabited-subtype P))
      ( λ Q  is-prop-type-trunc-Prop)
      ( subtype-inhabited-subtype P)
      ( refl-has-same-elements-inhabited-subtype)
      ( is-inhabited-subtype-inhabited-subtype P)

  extensionality-inhabited-subtype :
    (Q : inhabited-subtype l2 A)  (P  Q) 
    has-same-elements-inhabited-subtype P Q
  extensionality-inhabited-subtype Q =
    ( extensionality-subtype
      ( subtype-inhabited-subtype P)
      ( subtype-inhabited-subtype Q)) ∘e
    ( extensionality-type-subtype' is-inhabited-subtype-Prop P Q)

  has-same-elements-eq-inhabited-subtype :
    (Q : inhabited-subtype l2 A) 
    (P  Q)  has-same-elements-inhabited-subtype P Q
  has-same-elements-eq-inhabited-subtype Q =
    map-equiv (extensionality-inhabited-subtype Q)

  eq-has-same-elements-inhabited-subtype :
    (Q : inhabited-subtype l2 A) 
    has-same-elements-inhabited-subtype P Q  P  Q
  eq-has-same-elements-inhabited-subtype Q =
    map-inv-equiv (extensionality-inhabited-subtype Q)

  refl-extensionality-inhabited-subtype :
    map-equiv (extensionality-inhabited-subtype P) refl   x  pair id id)
  refl-extensionality-inhabited-subtype = refl