Trivial Σ-Decompositions

module foundation.trivial-sigma-decompositions where

open import foundation.contractible-types
open import foundation.equivalences
open import foundation.functoriality-propositional-truncation
open import foundation.inhabited-types
open import foundation.sigma-decompositions
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type

open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.functions
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.subtypes
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Definitions

module _
  {l1 : Level} (l2 : Level) (A : UU l1)
  where

  trivial-inhabited-Σ-Decomposition :
    (p : is-inhabited A) → Σ-Decomposition l2 l1 A
  pr1 (trivial-inhabited-Σ-Decomposition p) = raise-unit l2
  pr1 (pr2 (trivial-inhabited-Σ-Decomposition p)) = λ _ → (A , p)
  pr2 (pr2 (trivial-inhabited-Σ-Decomposition p)) =
    inv-left-unit-law-Σ-is-contr
      ( is-contr-raise-unit)
      ( raise-star)

  trivial-empty-Σ-Decomposition :
    (p : is-empty A) → Σ-Decomposition lzero lzero A
  pr1 (trivial-empty-Σ-Decomposition p) = empty
  pr1 (pr2 (trivial-empty-Σ-Decomposition p)) = ex-falso
  pr2 (pr2 (trivial-empty-Σ-Decomposition p)) =
    equiv-is-empty
      ( p)
      ( map-left-absorption-Σ _)

module _
  {l1 l2 l3 : Level} {A : UU l1}
  (D : Σ-Decomposition l2 l3 A)
  where

  is-trivial-Prop-Σ-Decomposition : Prop l2
  is-trivial-Prop-Σ-Decomposition =
    is-contr-Prop (indexing-type-Σ-Decomposition D)

  is-trivial-Σ-Decomposition : UU l2
  is-trivial-Σ-Decomposition = type-Prop is-trivial-Prop-Σ-Decomposition

is-trivial-trivial-inhabited-Σ-Decomposition :
  {l1 l2 : Level} {A : UU l1} (p : is-inhabited A)→
  is-trivial-Σ-Decomposition (trivial-inhabited-Σ-Decomposition l2 A p)
is-trivial-trivial-inhabited-Σ-Decomposition p = is-contr-raise-unit

type-trivial-Σ-Decomposition :
  {l1 l2 l3 : Level} {A : UU l1} → UU (l1 ⊔ lsuc l2 ⊔ lsuc l3)
type-trivial-Σ-Decomposition {l1} {l2} {l3} {A}=
  type-subtype (is-trivial-Prop-Σ-Decomposition {l1} {l2} {l3} {A})

Propositions

module _
  {l1 l2 l3 l4 : Level} {A : UU l1}
  (D : Σ-Decomposition l2 l3 A)
  ( is-trivial : is-trivial-Σ-Decomposition D)
  where

  is-inhabited-base-type-is-trivial-Σ-Decomposition :
    is-inhabited A
  is-inhabited-base-type-is-trivial-Σ-Decomposition =
    map-equiv-trunc-Prop
      ( inv-equiv (matching-correspondence-Σ-Decomposition D) ∘e
        inv-left-unit-law-Σ-is-contr is-trivial ( center is-trivial))
      ( is-inhabited-cotype-Σ-Decomposition D ( center is-trivial))

  equiv-trivial-is-trivial-Σ-Decomposition :
    equiv-Σ-Decomposition D
      ( trivial-inhabited-Σ-Decomposition
        ( l4)
        ( A)
        ( is-inhabited-base-type-is-trivial-Σ-Decomposition))
  pr1 equiv-trivial-is-trivial-Σ-Decomposition =
    ( map-equiv (compute-raise-unit l4) ∘ terminal-map ,
      is-equiv-comp
        ( map-equiv (compute-raise-unit l4))
        ( terminal-map)
        ( is-equiv-terminal-map-is-contr is-trivial)
        ( is-equiv-map-equiv ( compute-raise-unit l4)))
  pr1 (pr2 equiv-trivial-is-trivial-Σ-Decomposition) =
    ( λ x →
      ( ( inv-equiv (matching-correspondence-Σ-Decomposition D)) ∘e
        ( inv-left-unit-law-Σ-is-contr is-trivial x)))
  pr2 (pr2 equiv-trivial-is-trivial-Σ-Decomposition) a =
    eq-pair-Σ
      ( refl)
      ( inv-map-eq-transpose-equiv
        ( inv-equiv (matching-correspondence-Σ-Decomposition D))
        ( refl))

is-contr-type-trivial-Σ-Decomposition :
  {l1 l2 : Level} {A : UU l1} →
  (p : is-inhabited A) →
  is-contr (type-trivial-Σ-Decomposition {l1} {l2} {l1} {A})
pr1 ( is-contr-type-trivial-Σ-Decomposition {l1} {l2} {A} p) =
  ( trivial-inhabited-Σ-Decomposition l2 A p ,
    is-trivial-trivial-inhabited-Σ-Decomposition p)
pr2 ( is-contr-type-trivial-Σ-Decomposition {l1} {l2} {A} p) =
   ( λ x →
     eq-type-subtype
       ( is-trivial-Prop-Σ-Decomposition)
       ( inv
         ( eq-equiv-Σ-Decomposition
           ( pr1 x)
           ( trivial-inhabited-Σ-Decomposition l2 A p)
           ( equiv-trivial-is-trivial-Σ-Decomposition (pr1 x) (pr2 x)))))