1-Types

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

Created on 2022-01-26.
Last modified on 2024-02-06.

module foundation.1-types where

open import foundation-core.1-types public
Imports 
open import foundation.dependent-pair-types
open import foundation.subuniverses
open import foundation.truncated-types
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.equivalences
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.subtypes
open import foundation-core.torsorial-type-families
open import foundation-core.truncation-levels

Being a 1-type is a property

abstract
  is-prop-is-1-type :
    {l : Level} (A : UU l) → is-prop (is-1-type A)
  is-prop-is-1-type A = is-prop-is-trunc one-𝕋 A

is-1-type-Prop :
  {l : Level} → UU l → Prop l
is-1-type-Prop = is-trunc-Prop one-𝕋

The type of all 1-types in a universe is a 2-type

is-trunc-1-Type : {l : Level} → is-trunc two-𝕋 (1-Type l)
is-trunc-1-Type = is-trunc-Truncated-Type one-𝕋

1-Type-Truncated-Type : (l : Level) → Truncated-Type (lsuc l) two-𝕋
1-Type-Truncated-Type l = Truncated-Type-Truncated-Type l one-𝕋

Products of families of 1-types are 1-types

abstract
  is-1-type-Π :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    ((x : A) → is-1-type (B x)) → is-1-type ((x : A) → B x)
  is-1-type-Π = is-trunc-Π one-𝕋

type-Π-1-Type' :
  {l1 l2 : Level} (A : UU l1) (B : A → 1-Type l2) → UU (l1 ⊔ l2)
type-Π-1-Type' A B = (x : A) → type-1-Type (B x)

is-1-type-type-Π-1-Type' :
  {l1 l2 : Level} (A : UU l1) (B : A → 1-Type l2) →
  is-1-type (type-Π-1-Type' A B)
is-1-type-type-Π-1-Type' A B =
  is-1-type-Π (λ x → is-1-type-type-1-Type (B x))

Π-1-Type' :
  {l1 l2 : Level} (A : UU l1) (B : A → 1-Type l2) → 1-Type (l1 ⊔ l2)
pr1 (Π-1-Type' A B) = type-Π-1-Type' A B
pr2 (Π-1-Type' A B) = is-1-type-type-Π-1-Type' A B

type-Π-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : type-1-Type A → 1-Type l2) →
  UU (l1 ⊔ l2)
type-Π-1-Type A = type-Π-1-Type' (type-1-Type A)

is-1-type-type-Π-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : type-1-Type A → 1-Type l2) →
  is-1-type (type-Π-1-Type A B)
is-1-type-type-Π-1-Type A = is-1-type-type-Π-1-Type' (type-1-Type A)

Π-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : type-1-Type A → 1-Type l2) →
  1-Type (l1 ⊔ l2)
Π-1-Type = Π-Truncated-Type one-𝕋

The type of functions into a 1-type is a 1-type

abstract
  is-1-type-function-type :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-1-type B → is-1-type (A → B)
  is-1-type-function-type = is-trunc-function-type one-𝕋

type-hom-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : 1-Type l2) → UU (l1 ⊔ l2)
type-hom-1-Type A B = type-1-Type A → type-1-Type B

is-1-type-type-hom-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : 1-Type l2) →
  is-1-type (type-hom-1-Type A B)
is-1-type-type-hom-1-Type A B =
  is-1-type-function-type (is-1-type-type-1-Type B)

hom-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : 1-Type l2) → 1-Type (l1 ⊔ l2)
hom-1-Type = hom-Truncated-Type one-𝕋

1-Types are closed under dependent pair types

abstract
  is-1-type-Σ :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-1-type A → ((x : A) → is-1-type (B x)) → is-1-type (Σ A B)
  is-1-type-Σ = is-trunc-Σ {k = one-𝕋}

Σ-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : pr1 A → 1-Type l2) → 1-Type (l1 ⊔ l2)
Σ-1-Type = Σ-Truncated-Type

1-Types are closed under cartesian product types

abstract
  is-1-type-product :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} →
    is-1-type A → is-1-type B → is-1-type (A × B)
  is-1-type-product = is-trunc-product one-𝕋

product-1-Type :
  {l1 l2 : Level} (A : 1-Type l1) (B : 1-Type l2) → 1-Type (l1 ⊔ l2)
product-1-Type A B = Σ-1-Type A (λ x → B)

Subtypes of 1-types are 1-types

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

  abstract
    is-1-type-type-subtype : is-1-type A → is-1-type (type-subtype P)
    is-1-type-type-subtype = is-trunc-type-subtype zero-𝕋 P

module _
  {l : Level} (X : 1-Type l)
  where

  type-equiv-1-Type : {l2 : Level} (Y : 1-Type l2) → UU (l ⊔ l2)
  type-equiv-1-Type Y = type-1-Type X ≃ type-1-Type Y

  equiv-eq-1-Type : (Y : 1-Type l) → X ＝ Y → type-equiv-1-Type Y
  equiv-eq-1-Type = equiv-eq-subuniverse is-1-type-Prop X

  abstract
    is-torsorial-equiv-1-Type :
      is-torsorial (λ (Y : 1-Type l) → type-equiv-1-Type Y)
    is-torsorial-equiv-1-Type =
      is-torsorial-equiv-subuniverse is-1-type-Prop X

  abstract
    is-equiv-equiv-eq-1-Type : (Y : 1-Type l) → is-equiv (equiv-eq-1-Type Y)
    is-equiv-equiv-eq-1-Type = is-equiv-equiv-eq-subuniverse is-1-type-Prop X

  extensionality-1-Type :
    (Y : 1-Type l) → (X ＝ Y) ≃ type-equiv-1-Type Y
  pr1 (extensionality-1-Type Y) = equiv-eq-1-Type Y
  pr2 (extensionality-1-Type Y) = is-equiv-equiv-eq-1-Type Y

  eq-equiv-1-Type : (Y : 1-Type l) → type-equiv-1-Type Y → X ＝ Y
  eq-equiv-1-Type Y = eq-equiv-subuniverse is-1-type-Prop

Recent changes