Mere equivalences of types equipped with endomorphisms

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

Created on 2022-05-07.
Last modified on 2023-11-24.

module structured-types.mere-equivalences-types-equipped-with-endomorphisms where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import structured-types.equivalences-types-equipped-with-endomorphisms
open import structured-types.types-equipped-with-endomorphisms

Definition

Mere equivalences of types equipped with endomorphisms

module _
  {l1 l2 : Level}
  (X : Type-With-Endomorphism l1)
  (Y : Type-With-Endomorphism l2)
  where

  mere-equiv-prop-Type-With-Endomorphism : Prop (l1 ⊔ l2)
  mere-equiv-prop-Type-With-Endomorphism =
    trunc-Prop (equiv-Type-With-Endomorphism X Y)

  mere-equiv-Type-With-Endomorphism : UU (l1 ⊔ l2)
  mere-equiv-Type-With-Endomorphism =
    type-Prop mere-equiv-prop-Type-With-Endomorphism

  is-prop-mere-equiv-Type-With-Endomorphism :
    is-prop mere-equiv-Type-With-Endomorphism
  is-prop-mere-equiv-Type-With-Endomorphism =
    is-prop-type-Prop mere-equiv-prop-Type-With-Endomorphism

Refleivity of mere equivalences of types equipped with endomorphisms

module _
  {l1 : Level} (X : Type-With-Endomorphism l1)
  where

  refl-mere-equiv-Type-With-Endomorphism : mere-equiv-Type-With-Endomorphism X X
  refl-mere-equiv-Type-With-Endomorphism =
    unit-trunc-Prop (id-equiv-Type-With-Endomorphism X)

Components of the universe of types equipped with endomorphisms

module _
  {l1 : Level} (X : Type-With-Endomorphism l1)
  where

  Component-Type-With-Endomorphism : UU (lsuc l1)
  Component-Type-With-Endomorphism =
    Σ (Type-With-Endomorphism l1) (mere-equiv-Type-With-Endomorphism X)

  endo-Component-Type-With-Endomorphism :
    Component-Type-With-Endomorphism → Type-With-Endomorphism l1
  endo-Component-Type-With-Endomorphism = pr1

  type-Component-Type-With-Endomorphism :
    Component-Type-With-Endomorphism → UU l1
  type-Component-Type-With-Endomorphism =
    pr1 ∘ endo-Component-Type-With-Endomorphism

  endomorphism-Component-Type-With-Endomorphism :
    (T : Component-Type-With-Endomorphism) →
    type-Component-Type-With-Endomorphism T →
    type-Component-Type-With-Endomorphism T
  endomorphism-Component-Type-With-Endomorphism T =
    pr2 (endo-Component-Type-With-Endomorphism T)

  mere-equiv-Component-Type-With-Endomorphism :
    (T : Component-Type-With-Endomorphism) →
    mere-equiv-Type-With-Endomorphism X
      ( endo-Component-Type-With-Endomorphism T)
  mere-equiv-Component-Type-With-Endomorphism T = pr2 T

  canonical-Component-Type-With-Endomorphism : Component-Type-With-Endomorphism
  pr1 canonical-Component-Type-With-Endomorphism = X
  pr2 canonical-Component-Type-With-Endomorphism =
    refl-mere-equiv-Type-With-Endomorphism X

Equivalences of types equipped with an endomorphism in a given component

module _
  {l1 : Level} (X : Type-With-Endomorphism l1)
  where

  equiv-Component-Type-With-Endomorphism :
    (T S : Component-Type-With-Endomorphism X) → UU l1
  equiv-Component-Type-With-Endomorphism T S =
    equiv-Type-With-Endomorphism
      ( endo-Component-Type-With-Endomorphism X T)
      ( endo-Component-Type-With-Endomorphism X S)

  id-equiv-Component-Type-With-Endomorphism :
    ( T : Component-Type-With-Endomorphism X) →
    equiv-Component-Type-With-Endomorphism T T
  id-equiv-Component-Type-With-Endomorphism T =
    id-equiv-Type-With-Endomorphism (endo-Component-Type-With-Endomorphism X T)

  equiv-eq-Component-Type-With-Endomorphism :
    (T S : Component-Type-With-Endomorphism X) →
    T ＝ S → equiv-Component-Type-With-Endomorphism T S
  equiv-eq-Component-Type-With-Endomorphism T .T refl =
    id-equiv-Component-Type-With-Endomorphism T

  is-torsorial-equiv-Component-Type-With-Endomorphism :
    is-torsorial
      ( equiv-Component-Type-With-Endomorphism
        ( canonical-Component-Type-With-Endomorphism X))
  is-torsorial-equiv-Component-Type-With-Endomorphism =
    is-torsorial-Eq-subtype
      ( is-torsorial-equiv-Type-With-Endomorphism X)
      ( λ Y → is-prop-type-trunc-Prop)
      ( X)
      ( id-equiv-Type-With-Endomorphism X)
      ( refl-mere-equiv-Type-With-Endomorphism X)

  is-equiv-equiv-eq-Component-Type-With-Endomorphism :
    (T : Component-Type-With-Endomorphism X) →
    is-equiv
      ( equiv-eq-Component-Type-With-Endomorphism
        ( canonical-Component-Type-With-Endomorphism X)
        ( T))
  is-equiv-equiv-eq-Component-Type-With-Endomorphism =
    fundamental-theorem-id
      ( is-torsorial-equiv-Component-Type-With-Endomorphism)
      ( equiv-eq-Component-Type-With-Endomorphism
        ( canonical-Component-Type-With-Endomorphism X))

Recent changes