The symmetric identity types

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

Created on 2023-01-31.
Last modified on 2024-02-08.

module foundation.symmetric-identity-types where
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.functoriality-dependent-function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.universe-levels
open import foundation.unordered-pairs

open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.torsorial-type-families

open import univalent-combinatorics.standard-finite-types

Idea

We construct a variant of the identity type equipped with a natural ℤ/2-action.

Definition

module _
  {l : Level} {A : UU l}
  where

  symmetric-Id :
    (a : unordered-pair A)  UU l
  symmetric-Id a =
    Σ A  x  (i : type-unordered-pair a)  x  element-unordered-pair a i)

  module _
    (a : unordered-pair A)
    where

    Eq-symmetric-Id :
      (p q : symmetric-Id a)  UU l
    Eq-symmetric-Id (x , H) q =
      Σ (x  pr1 q)  p  (i : type-unordered-pair a)  H i  (p  pr2 q i))

    refl-Eq-symmetric-Id :
      (p : symmetric-Id a)  Eq-symmetric-Id p p
    pr1 (refl-Eq-symmetric-Id (x , H)) = refl
    pr2 (refl-Eq-symmetric-Id (x , H)) i = refl

    is-torsorial-Eq-symmetric-Id :
      (p : symmetric-Id a)  is-torsorial (Eq-symmetric-Id p)
    is-torsorial-Eq-symmetric-Id (x , H) =
      is-torsorial-Eq-structure
        ( is-torsorial-Id x)
        ( x , refl)
        ( is-torsorial-htpy H)

    Eq-eq-symmetric-Id :
      (p q : symmetric-Id a)  p  q  Eq-symmetric-Id p q
    Eq-eq-symmetric-Id p .p refl = refl-Eq-symmetric-Id p

    is-equiv-Eq-eq-symmetric-Id :
      (p q : symmetric-Id a)  is-equiv (Eq-eq-symmetric-Id p q)
    is-equiv-Eq-eq-symmetric-Id p =
      fundamental-theorem-id
        ( is-torsorial-Eq-symmetric-Id p)
        ( Eq-eq-symmetric-Id p)

    extensionality-symmetric-Id :
      (p q : symmetric-Id a)  (p  q)  Eq-symmetric-Id p q
    pr1 (extensionality-symmetric-Id p q) = Eq-eq-symmetric-Id p q
    pr2 (extensionality-symmetric-Id p q) = is-equiv-Eq-eq-symmetric-Id p q

    eq-Eq-symmetric-Id :
      (p q : symmetric-Id a)  Eq-symmetric-Id p q  p  q
    eq-Eq-symmetric-Id p q = map-inv-equiv (extensionality-symmetric-Id p q)

  module _
    (a b : A)
    where

    map-compute-symmetric-Id :
      symmetric-Id (standard-unordered-pair a b)  a  b
    map-compute-symmetric-Id (x , f) = inv (f (zero-Fin 1))  f (one-Fin 1)

    map-inv-compute-symmetric-Id :
      a  b  symmetric-Id (standard-unordered-pair a b)
    pr1 (map-inv-compute-symmetric-Id p) = a
    pr2 (map-inv-compute-symmetric-Id p) (inl (inr _)) = refl
    pr2 (map-inv-compute-symmetric-Id p) (inr _) = p

    is-section-map-inv-compute-symmetric-Id :
      ( map-compute-symmetric-Id  map-inv-compute-symmetric-Id) ~ id
    is-section-map-inv-compute-symmetric-Id refl = refl

    abstract
      is-retraction-map-inv-compute-symmetric-Id :
        ( map-inv-compute-symmetric-Id  map-compute-symmetric-Id) ~ id
      is-retraction-map-inv-compute-symmetric-Id (x , f) =
        eq-Eq-symmetric-Id
          ( standard-unordered-pair a b)
          ( map-inv-compute-symmetric-Id (map-compute-symmetric-Id (x , f)))
          ( x , f)
          ( ( inv (f (zero-Fin 1))) ,
            ( λ where
              ( inl (inr _))  inv (left-inv (f (zero-Fin 1)))
              ( inr _)  refl))

    is-equiv-map-compute-symmetric-Id :
      is-equiv (map-compute-symmetric-Id)
    is-equiv-map-compute-symmetric-Id =
      is-equiv-is-invertible
        ( map-inv-compute-symmetric-Id)
        ( is-section-map-inv-compute-symmetric-Id)
        ( is-retraction-map-inv-compute-symmetric-Id)

    compute-symmetric-Id :
      symmetric-Id (standard-unordered-pair a b)  (a  b)
    pr1 (compute-symmetric-Id) = map-compute-symmetric-Id
    pr2 (compute-symmetric-Id) = is-equiv-map-compute-symmetric-Id

Properties

The action of functions on symmetric identity types

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  map-symmetric-Id :
    (f : A  B) (a : unordered-pair A) 
    symmetric-Id a  symmetric-Id (map-unordered-pair f a)
  map-symmetric-Id f a =
    map-Σ
      ( λ b  (x : type-unordered-pair a)  b  f (element-unordered-pair a x))
      ( f)
      ( λ x  map-Π  i  ap f))

The action of equivalences on symmetric identity types

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}
  where

  equiv-symmetric-Id :
    (e : A  B) (a : unordered-pair A) 
    symmetric-Id a  symmetric-Id (map-equiv-unordered-pair e a)
  equiv-symmetric-Id e a =
    equiv-Σ
      ( λ b 
        (x : type-unordered-pair a) 
        b  map-equiv e (element-unordered-pair a x))
      ( e)
      ( λ x 
        equiv-Π-equiv-family  i  equiv-ap e x (element-unordered-pair a i)))

  map-equiv-symmetric-Id :
    (e : A  B) (a : unordered-pair A) 
    symmetric-Id a  symmetric-Id (map-equiv-unordered-pair e a)
  map-equiv-symmetric-Id e a = map-equiv (equiv-symmetric-Id e a)

id-equiv-symmetric-Id :
  {l : Level} {A : UU l} (a : unordered-pair A) 
  map-equiv-symmetric-Id id-equiv a ~ id
id-equiv-symmetric-Id a (x , H) =
  eq-pair-eq-fiber (eq-htpy  u  ap-id (H u)))

Transport in the symmetric identity type along observational equality of unordered pairs

module _
  {l : Level} {A : UU l}
  where

  equiv-tr-symmetric-Id :
    (p q : unordered-pair A)  Eq-unordered-pair p q 
    symmetric-Id p  symmetric-Id q
  equiv-tr-symmetric-Id (X , f) (Y , g) (e , H) =
    equiv-tot  a  equiv-Π  x  a  g x) e  x  equiv-concat' a (H x)))

  tr-symmetric-Id :
    (p q : unordered-pair A)
    (e : type-unordered-pair p  type-unordered-pair q) 
    (element-unordered-pair p ~ (element-unordered-pair q  map-equiv e)) 
    symmetric-Id p  symmetric-Id q
  tr-symmetric-Id p q e H = map-equiv (equiv-tr-symmetric-Id p q (pair e H))

  compute-pr2-tr-symmetric-Id :
    (p q : unordered-pair A)
    (e : type-unordered-pair p  type-unordered-pair q) 
    (H : element-unordered-pair p ~ (element-unordered-pair q  map-equiv e)) 
    {a : A}
    (K : (x : type-unordered-pair p)  a  element-unordered-pair p x) 
    (x : type-unordered-pair p) 
    pr2 (tr-symmetric-Id p q e H (a , K)) (map-equiv e x)  (K x  H x)
  compute-pr2-tr-symmetric-Id (X , f) (Y , g) e H {a} =
    compute-map-equiv-Π  x  a  g x) e  x  equiv-concat' a (H x))

  refl-Eq-unordered-pair-tr-symmetric-Id :
    (p : unordered-pair A) 
    tr-symmetric-Id p p id-equiv refl-htpy ~ id
  refl-Eq-unordered-pair-tr-symmetric-Id p (a , K) =
    eq-pair-eq-fiber
      ( eq-htpy
        ( ( compute-pr2-tr-symmetric-Id p p id-equiv refl-htpy K) ∙h
          ( right-unit-htpy)))

Recent changes