Computational identity types

Content created by Fredrik Bakke.

Created on 2024-02-08.
Last modified on 2024-02-19.

module foundation.computational-identity-types where

Imports

open import foundation.action-on-identifications-binary-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.function-extensionality
open import foundation.strictly-right-unital-concatenation-identifications
open import foundation.transport-along-identifications
open import foundation.univalence
open import foundation.universal-property-identity-systems
open import foundation.universe-levels
open import foundation.yoneda-identity-types

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-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.identity-types
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.torsorial-type-families

Idea

The standard definition of identity types has the limitation that many of the basic operations only satisfy algebraic laws weakly. On this page, we consider the computational identity types^¶ x ＝ʲ y, whose elements we call computational identifications^¶. These are defined using the construction of the strictly involutive identity types:

  (x ＝ⁱ y) := Σ (z : A) ((z ＝ y) × (z ＝ x))

but using the Yoneda identity types (_＝ʸ_) as the underlying identity types:

  (x ＝ʸ y) := (z : A) → (z ＝ x) → (z ＝ y),

hence, their definition is

  (x ＝ʲ y) := Σ (z : A) ((z ＝ʸ y) × (z ＝ʸ x)).

The Yoneda identity types are equivalent to the standard identity types, but have a strictly associative and unital concatenation operation. We can leverage this and the strictness properties of the construction of the strictly involutive identity types to construct operations on the computational identity types that satisfy the strict algebraic laws

(p ∙ʲ q) ∙ʲ r ≐ p ∙ʲ (q ∙ʲ r)
reflʲ ∙ʲ p ≐ p or p ∙ʲ reflʲ ≐ p
invʲ (invʲ p) ≐ p
invʲ reflʲ ≐ reflʲ.

While the last three equalities hold by the same computations as for the strictly involutive identity types using the fact that invʸ reflʸ ≐ reflʸ, strict associativity relies on the strict associativity of the underlying Yoneda identity types. See the file about strictly involutive identity types for further details on computations related to the last three equalities. In addition to these strict algebraic laws, we also define a recursion principle for the computational identity types that computes strictly.

Note. The computational identity types do not satisfy the strict laws

reflʲ ∙ʲ p ≐ p and p ∙ʲ reflʲ ≐ p simultaneously,
invʲ p ∙ʲ p ≐ reflʲ, or
p ∙ʲ invʲ p ≐ reflʲ,

and they do not have a strict computation property for their induction principle. This boils down to the fact that the Yoneda identity types do not have a strict computation property for their induction principle, which is explained further there.

Definition

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

  computational-Id : (x y : A) → UU l
  computational-Id x y = Σ A (λ z → (z ＝ʸ y) × (z ＝ʸ x))

  infix 6 _＝ʲ_
  _＝ʲ_ : A → A → UU l
  (a ＝ʲ b) = computational-Id a b

  reflʲ : {x : A} → x ＝ʲ x
  reflʲ {x} = (x , reflʸ , reflʸ)

Properties

The computational identity types are equivalent to the Yoneda identity types

The computational identity types are equivalent to the Yoneda identity types, and similarly to the strictly involutive identity types, this equivalence is a strict retraction and preserves the reflexivities strictly.

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

  computational-eq-yoneda-eq : {x y : A} → x ＝ʸ y → x ＝ʲ y
  computational-eq-yoneda-eq {x} f = (x , f , reflʸ)

  yoneda-eq-computational-eq : {x y : A} → x ＝ʲ y → x ＝ʸ y
  yoneda-eq-computational-eq (z , p , q) = invʸ q ∙ʸ p

  is-retraction-yoneda-eq-computational-eq :
    {x y : A} →
    is-retraction
      ( computational-eq-yoneda-eq)
      ( yoneda-eq-computational-eq {x} {y})
  is-retraction-yoneda-eq-computational-eq f = refl

  is-section-yoneda-eq-computational-eq :
    {x y : A} →
    is-section
      ( computational-eq-yoneda-eq)
      ( yoneda-eq-computational-eq {x} {y})
  is-section-yoneda-eq-computational-eq (z , p , q) =
    ind-yoneda-Id
      ( λ _ q →
        computational-eq-yoneda-eq (yoneda-eq-computational-eq (z , p , q)) ＝
        (z , p , q))
      ( refl)
      ( q)

  is-equiv-computational-eq-yoneda-eq :
    {x y : A} → is-equiv (computational-eq-yoneda-eq {x} {y})
  is-equiv-computational-eq-yoneda-eq =
    is-equiv-is-invertible
      ( yoneda-eq-computational-eq)
      ( is-section-yoneda-eq-computational-eq)
      ( is-retraction-yoneda-eq-computational-eq)

  is-equiv-yoneda-eq-computational-eq :
    {x y : A} → is-equiv (yoneda-eq-computational-eq {x} {y})
  is-equiv-yoneda-eq-computational-eq =
    is-equiv-is-invertible
      ( computational-eq-yoneda-eq)
      ( is-retraction-yoneda-eq-computational-eq)
      ( is-section-yoneda-eq-computational-eq)

  equiv-computational-eq-yoneda-eq : {x y : A} → (x ＝ʸ y) ≃ (x ＝ʲ y)
  pr1 equiv-computational-eq-yoneda-eq = computational-eq-yoneda-eq
  pr2 equiv-computational-eq-yoneda-eq = is-equiv-computational-eq-yoneda-eq

  equiv-yoneda-eq-computational-eq : {x y : A} → (x ＝ʲ y) ≃ (x ＝ʸ y)
  pr1 equiv-yoneda-eq-computational-eq = yoneda-eq-computational-eq
  pr2 equiv-yoneda-eq-computational-eq = is-equiv-yoneda-eq-computational-eq

This equivalence preserves the reflexivity elements strictly in both directions.

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

  preserves-refl-yoneda-eq-computational-eq :
    {x : A} →
    yoneda-eq-computational-eq (reflʲ {x = x}) ＝ reflʸ
  preserves-refl-yoneda-eq-computational-eq = refl

  preserves-refl-computational-eq-yoneda-eq :
    {x : A} →
    computational-eq-yoneda-eq (reflʸ {x = x}) ＝ reflʲ
  preserves-refl-computational-eq-yoneda-eq = refl

The computational identity types are equivalent to the standard identity types

By the composite equivalence (x ＝ y) ≃ (x ＝ʸ y) ≃ (x ＝ʲ y), the computational identity types are equivalent to the standard identity types. Since each of these equivalences preserve the groupoid structure weakly, so does the composite. For the same reason, it preserves the reflexivities strictly.

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

  computational-eq-eq : {x y : A} → x ＝ y → x ＝ʲ y
  computational-eq-eq = computational-eq-yoneda-eq ∘ yoneda-eq-eq

  eq-computational-eq : {x y : A} → x ＝ʲ y → x ＝ y
  eq-computational-eq = eq-yoneda-eq ∘ yoneda-eq-computational-eq

  equiv-computational-eq-eq : {x y : A} → (x ＝ y) ≃ (x ＝ʲ y)
  equiv-computational-eq-eq =
    equiv-computational-eq-yoneda-eq ∘e equiv-yoneda-eq-eq

  equiv-eq-computational-eq : {x y : A} → (x ＝ʲ y) ≃ (x ＝ y)
  equiv-eq-computational-eq =
    equiv-eq-yoneda-eq ∘e equiv-yoneda-eq-computational-eq

  is-retraction-eq-computational-eq :
    {x y : A} → is-retraction computational-eq-eq (eq-computational-eq {x} {y})
  is-retraction-eq-computational-eq p = left-unit-right-strict-concat

  is-section-eq-computational-eq :
    {x y : A} →
    is-section computational-eq-eq (eq-computational-eq {x} {y})
  is-section-eq-computational-eq (z , p , q) =
    ind-yoneda-Id
      ( λ _ q →
        computational-eq-eq (eq-computational-eq (z , p , q)) ＝ (z , p , q))
      ( eq-pair-eq-fiber (eq-pair (is-section-eq-yoneda-eq p) refl))
      ( q)

  is-equiv-computational-eq-eq :
    {x y : A} → is-equiv (computational-eq-eq {x} {y})
  is-equiv-computational-eq-eq = is-equiv-map-equiv equiv-computational-eq-eq

  is-equiv-eq-computational-eq :
    {x y : A} → is-equiv (eq-computational-eq {x} {y})
  is-equiv-eq-computational-eq = is-equiv-map-equiv equiv-eq-computational-eq

This equivalence preserves the reflexivity elements strictly in both directions.

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

  preserves-refl-computational-eq-eq :
    {x : A} → computational-eq-eq (refl {x = x}) ＝ reflʲ
  preserves-refl-computational-eq-eq = refl

  preserves-refl-eq-computational-eq :
    {x : A} → eq-computational-eq (reflʲ {x = x}) ＝ refl
  preserves-refl-eq-computational-eq = refl

Torsoriality of the computational identity types

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

  is-torsorial-computational-Id : is-torsorial (computational-Id x)
  is-torsorial-computational-Id =
    is-contr-equiv
      ( Σ A (x ＝_))
      ( equiv-tot (λ y → equiv-eq-computational-eq {x = x} {y}))
      ( is-torsorial-Id x)

The dependent universal property of the computational identity types

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

  dependent-universal-property-identity-system-computational-Id :
    dependent-universal-property-identity-system
      ( computational-Id x)
      ( reflʲ)
  dependent-universal-property-identity-system-computational-Id =
    dependent-universal-property-identity-system-is-torsorial
      ( reflʲ)
      ( is-torsorial-computational-Id)

The induction principle for the computational identity types

The computational identity types satisfy the induction principle of the identity types. This states that given a base point x : A and a family of types over the identity types based at x, B : (y : A) (p : x ＝ʲ y) → UU l2, then to construct a dependent function f : (y : A) (p : x ＝ʲ y) → B y p it suffices to define it at f x reflʲ.

module _
  {l1 l2 : Level} {A : UU l1} {x : A}
  (B : (y : A) (p : x ＝ʲ y) → UU l2)
  where

  ind-computational-Id :
    (b : B x reflʲ) {y : A} (p : x ＝ʲ y) → B y p
  ind-computational-Id b {y} =
    map-inv-is-equiv
      ( dependent-universal-property-identity-system-computational-Id B)
      ( b)
      ( y)

  compute-ind-computational-Id :
    (b : B x reflʲ) → ind-computational-Id b reflʲ ＝ b
  compute-ind-computational-Id =
    is-section-map-inv-is-equiv
      ( dependent-universal-property-identity-system-computational-Id B)

  uniqueness-ind-computational-Id :
    (b : (y : A) (p : x ＝ʲ y) → B y p) →
    (λ y → ind-computational-Id (b x reflʲ) {y}) ＝ b
  uniqueness-ind-computational-Id =
    is-retraction-map-inv-is-equiv
      ( dependent-universal-property-identity-system-computational-Id B)

The strict recursion principle for the computational identity types

Using the fact that the recusion principles of both the Yoneda identity types and the strictly involutive identity types can be defined to compute strictly, we obtain a strictly computing recursion principle for the computational identity types as well.

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

  rec-computational-Id :
    (b : B x) {y : A} → x ＝ʲ y → B y
  rec-computational-Id b p = rec-yoneda-Id b (yoneda-eq-computational-eq p)

  compute-rec-computational-Id :
    (b : B x) → rec-computational-Id b reflʲ ＝ b
  compute-rec-computational-Id b = refl

  uniqueness-rec-computational-Id :
    (b : (y : A) → x ＝ʲ y → B y) →
    (λ y → rec-computational-Id (b x reflʲ) {y}) ＝ b
  uniqueness-rec-computational-Id b =
    ( inv
      ( uniqueness-ind-computational-Id
        ( λ y _ → B y)
        ( λ y → rec-computational-Id (b x reflʲ)))) ∙
    ( uniqueness-ind-computational-Id (λ y _ → B y) b)

Structure

The computational identity types form a groupoidal structure on types. This structure satisfies the following algebraic laws strictly

(p ∙ʲ q) ∙ʲ r ≐ p ∙ʲ (q ∙ʲ r)
reflʲ ∙ʲ p ≐ p or p ∙ʲ reflʲ ≐ p
invʲ (invʲ p) ≐ p
invʲ reflʲ ≐ reflʲ.

Inverting computational identifications

The construction and computations are the same as for the strictly involutive identity types. Thus, the inversion operation is defined by swapping the positions of the two Yoneda identifications

  invʲ := (z , p , q) ↦ (z , q , p).

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

  invʲ : {x y : A} → x ＝ʲ y → y ＝ʲ x
  invʲ (z , p , q) = (z , q , p)

  compute-inv-refl-computational-Id :
    {x : A} → invʲ (reflʲ {x = x}) ＝ reflʲ
  compute-inv-refl-computational-Id = refl

  inv-inv-computational-Id :
    {x y : A} (p : x ＝ʲ y) →
    invʲ (invʲ p) ＝ p
  inv-inv-computational-Id p = refl

The inversion operation on computational identifications corresponds to the standard inversion operation on identifications:

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

  preserves-inv-computational-eq-eq :
    (p : x ＝ y) →
    computational-eq-eq (inv p) ＝ invʲ (computational-eq-eq p)
  preserves-inv-computational-eq-eq refl = refl

  preserves-inv-eq-computational-eq :
    (p : x ＝ʲ y) →
    eq-computational-eq (invʲ p) ＝ inv (eq-computational-eq p)
  preserves-inv-eq-computational-eq (z , f , g) =
    ( ap (g y) (left-unit-right-strict-concat)) ∙
    ( distributive-inv-Id-yoneda-Id g f) ∙
    ( ap (λ r → inv (f x r)) (inv left-unit-right-strict-concat))

The concatenation operations on computational identifications

There is both a strictly left unital and a strictly right unital concatenation operation, while both are strictly associative. The strict one-sided unitality follows in both cases from the strict right unitality of the concatenation operation on the Yoneda identifications, following the same computation as for the strictly involutive identity types. For associativity on the other hand, we must use the strict associativity of the Yoneda identity types. We will write out the explicit computation later.

Observation. Since the concatenation operations are strictly associative, every string of concatenations containing reflexivities will reduce aside from possibly when the reflexivity appears all the way to the right or left in the string.

The strictly left unital concatenation operation

The strictly left unital concatenation operation is constructed the same way as the strictly left unital concatenation operation for the strictly involutive identity types

  (w , p , q) ∙ʲ (w' , p' , q') := (w' , p' , q' ∙ʸ invʸ p ∙ʸ q)

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

  infixl 15 _∙ʲ_
  _∙ʲ_ : {x y z : A} → x ＝ʲ y → y ＝ʲ z → x ＝ʲ z
  (w , p , q) ∙ʲ (w' , p' , q') = (w' , p' , q' ∙ʸ invʸ p ∙ʸ q)

  concat-computational-Id : {x y : A} → x ＝ʲ y → (z : A) → y ＝ʲ z → x ＝ʲ z
  concat-computational-Id p z q = p ∙ʲ q

  concat-computational-Id' : (x : A) {y z : A} → y ＝ʲ z → x ＝ʲ y → x ＝ʲ z
  concat-computational-Id' x q p = p ∙ʲ q

The strictly left unital concatenation operation on computational identifications corresponds to the strictly left unital concatenation operation on standard identifications.

module _
  {l : Level} {A : UU l} {x y z : A}
  where

  preserves-concat-computational-eq-eq :
    (p : x ＝ y) (q : y ＝ z) →
    computational-eq-eq (p ∙ q) ＝
    computational-eq-eq p ∙ʲ computational-eq-eq q
  preserves-concat-computational-eq-eq refl q = refl

  preserves-concat-eq-computational-eq :
    (p : x ＝ʲ y) (q : y ＝ʲ z) →
    eq-computational-eq (p ∙ʲ q) ＝
    eq-computational-eq p ∙ eq-computational-eq q
  preserves-concat-eq-computational-eq (w , f , g) (w' , f' , g') =
    ( ap (f' x) left-unit-right-strict-concat) ∙
    ( ap
      ( f' x)
      ( ( ap
          ( inv)
          ( commutative-preconcatr-Id-yoneda-Id
            ( g)
            ( g' w' refl)
            ( inv (f w refl)))) ∙
        ( ( distributive-inv-right-strict-concat
            ( g' w' refl)
            ( g y (inv (f w refl)))) ∙
          ( ( ap
              ( _∙ᵣ inv (g' w' refl))
              ( inv-distributive-inv-Id-yoneda-Id f g)) ∙
            ( eq-concat-right-strict-concat
              ( f x (inv (g w refl)))
              ( inv (g' w' refl)))))) ∙
    ( commutative-preconcat-Id-yoneda-Id f'
      ( f x (inv (g w refl)))
      ( inv (g' w' refl)))) ∙
    ( ap-binary
      ( _∙_)
      ( ap (f x) (inv left-unit-right-strict-concat))
      ( ap (f' y) (inv left-unit-right-strict-concat)))

The strictly right unital concatenation operation

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

  infixl 15 _∙ᵣʲ_
  _∙ᵣʲ_ : {x y z : A} → x ＝ʲ y → y ＝ʲ z → x ＝ʲ z
  (w , p , q) ∙ᵣʲ (w' , p' , q') = (w , p ∙ʸ invʸ q' ∙ʸ p' , q)

  right-strict-concat-computational-Id :
    {x y : A} → x ＝ʲ y → (z : A) → y ＝ʲ z → x ＝ʲ z
  right-strict-concat-computational-Id p z q = p ∙ᵣʲ q

  right-strict-concat-computational-Id' :
    (x : A) {y z : A} → y ＝ʲ z → x ＝ʲ y → x ＝ʲ z
  right-strict-concat-computational-Id' x q p = p ∙ᵣʲ q

The strictly right unital concatenation operation on computational identifications corresponds to the strictly right unital concatenation operation on standard identifications.

module _
  {l : Level} {A : UU l} {x y z : A}
  where

  preserves-right-strict-concat-computational-eq-eq :
    (p : x ＝ y) (q : y ＝ z) →
    computational-eq-eq (p ∙ᵣ q) ＝
    computational-eq-eq p ∙ᵣʲ computational-eq-eq q
  preserves-right-strict-concat-computational-eq-eq p refl = refl

  preserves-right-strict-concat-eq-computational-eq :
    (p : x ＝ʲ y) (q : y ＝ʲ z) →
    eq-computational-eq (p ∙ᵣʲ q) ＝
    eq-computational-eq p ∙ᵣ eq-computational-eq q
  preserves-right-strict-concat-eq-computational-eq (w , f , g) (w' , f' , g') =
    ( ap
      ( λ r → f' x (f x r ∙ᵣ inv (g' w' refl)))
      ( left-unit-right-strict-concat)) ∙
    ( commutative-preconcatr-Id-yoneda-Id
      ( f')
      ( f x (inv (g w refl)))
      ( inv (g' w' refl))) ∙
    ( ap-binary
      ( _∙ᵣ_)
      ( ap (f x) (inv left-unit-right-strict-concat))
      ( ap (f' y) (inv left-unit-right-strict-concat)))

The groupoidal laws for the computational identity types

The groupoidal laws for the strictly left unital concatenation operation

To see that _∙ʲ_ is strictly associative, we unfold both (P ∙ʲ Q) ∙ʲ R and P ∙ʲ (Q ∙ʲ R) and observe that it follows from the strict associativity of _∙ʸ_:

  (P ∙ʲ Q) ∙ʲ R
  ≐ ((u , p , p') ∙ʲ (v , q , q')) ∙ʲ (w , r , r')
  ≐ ((v , q , (q' ∙ʸ invʸ p) ∙ʸ p')) ∙ʲ (w , r , r')
  ≐ (w , r , (r' ∙ʸ invʸ q) ∙ʸ ((q' ∙ʸ invʸ p) ∙ʸ p'))

  ≐ (w , r , (((r' ∙ʸ invʸ q) ∙ʸ q') ∙ʸ invʸ p) ∙ʸ p')
  ≐ (u , p , p') ∙ʲ ((w , r , (r' ∙ʸ invʸ q) ∙ʸ q'))
  ≐ (u , p , p') ∙ʲ ((v , q , q') ∙ʲ (w , r , r'))
  ≐ P ∙ʲ (Q ∙ʲ R).

module _
  {l : Level} {A : UU l} {x y z w : A}
  where

  assoc-concat-computational-Id :
    (p : x ＝ʲ y) (q : y ＝ʲ z) (r : z ＝ʲ w) →
    (p ∙ʲ q) ∙ʲ r ＝ p ∙ʲ (q ∙ʲ r)
  assoc-concat-computational-Id p q r = refl

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

  left-unit-concat-computational-Id :
    {p : x ＝ʲ y} → reflʲ ∙ʲ p ＝ p
  left-unit-concat-computational-Id = refl

  right-unit-concat-computational-Id :
    {p : x ＝ʲ y} → p ∙ʲ reflʲ ＝ p
  right-unit-concat-computational-Id {z , p , q} =
    ind-yoneda-Id
      ( λ _ p → (z , p , q) ∙ʲ reflʲ ＝ (z , p , q))
      ( refl)
      ( p)

  left-inv-concat-computational-Id :
    (p : x ＝ʲ y) → invʲ p ∙ʲ p ＝ reflʲ
  left-inv-concat-computational-Id (z , p , q) =
    ind-yoneda-Id
      ( λ _ p →
        ( invʲ (z , p , q) ∙ʲ (z , p , q)) ＝
        ( reflʲ))
      ( eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-yoneda-Id q)))
      ( p)

  right-inv-concat-computational-Id :
    (p : x ＝ʲ y) → p ∙ʲ invʲ p ＝ reflʲ
  right-inv-concat-computational-Id (z , p , q) =
    ind-yoneda-Id
      ( λ _ q →
        ( (z , p , q) ∙ʲ invʲ (z , p , q)) ＝
        ( reflʲ))
      ( eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-yoneda-Id p)))
      ( q)

  distributive-inv-concat-computational-Id :
    (p : x ＝ʲ y) {z : A} (q : y ＝ʲ z) →
    invʲ (p ∙ʲ q) ＝
    invʲ q ∙ʲ invʲ p
  distributive-inv-concat-computational-Id p =
    ind-computational-Id
      ( λ _ q →
        invʲ (p ∙ʲ q) ＝
        invʲ q ∙ʲ invʲ p)
      ( ap invʲ (right-unit-concat-computational-Id))

The groupoidal laws for the strictly right unital concatenation operation

Associativity for the strictly right unital concatenation operation follows from a similar computation to the one for the strictly left unital concatenation operation.

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

  assoc-right-strict-concat-computational-Id :
    {x y z w : A} (p : x ＝ʲ y) (q : y ＝ʲ z) (r : z ＝ʲ w) →
    (p ∙ᵣʲ q) ∙ᵣʲ r ＝ p ∙ᵣʲ (q ∙ᵣʲ r)
  assoc-right-strict-concat-computational-Id p q r = refl

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

  right-unit-right-strict-concat-computational-Id :
    {p : x ＝ʲ y} → p ∙ᵣʲ reflʲ ＝ p
  right-unit-right-strict-concat-computational-Id = refl

  left-unit-right-strict-concat-computational-Id :
    {p : x ＝ʲ y} → reflʲ ∙ᵣʲ p ＝ p
  left-unit-right-strict-concat-computational-Id {z , p , q} =
    ind-yoneda-Id (λ _ q → reflʲ ∙ᵣʲ (z , p , q) ＝ (z , p , q)) refl q

  left-inv-right-strict-concat-computational-Id :
    (p : x ＝ʲ y) → invʲ p ∙ᵣʲ p ＝ reflʲ
  left-inv-right-strict-concat-computational-Id (z , p , q) =
    ind-yoneda-Id
      ( λ _ p → invʲ (z , p , q) ∙ᵣʲ (z , p , q) ＝ reflʲ)
      ( eq-pair-eq-fiber (eq-pair (right-inv-yoneda-Id q) refl))
      ( p)

  right-inv-right-strict-concat-computational-Id :
    (p : x ＝ʲ y) → p ∙ᵣʲ invʲ p ＝ reflʲ
  right-inv-right-strict-concat-computational-Id (z , p , q) =
    ind-yoneda-Id
      ( λ _ q → (z , p , q) ∙ᵣʲ invʲ (z , p , q) ＝ reflʲ)
      ( eq-pair-eq-fiber (eq-pair (right-inv-yoneda-Id p) refl))
      ( q)

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

  distributive-inv-right-strict-concat-computational-Id :
    (p : x ＝ʲ y) {z : A} (q : y ＝ʲ z) → invʲ (p ∙ᵣʲ q) ＝ invʲ q ∙ᵣʲ invʲ p
  distributive-inv-right-strict-concat-computational-Id p =
    ind-computational-Id
      ( λ _ q → invʲ (p ∙ᵣʲ q) ＝ invʲ q ∙ᵣʲ invʲ p)
      ( inv left-unit-right-strict-concat-computational-Id)

Operations

We can define a range of basic operations on computational identifications that all enjoy strict computational properties.

Action of functions on computational identifications

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

  eq-ap-computational-Id : {x y : A} → x ＝ʲ y → f x ＝ f y
  eq-ap-computational-Id = ap f ∘ eq-computational-eq

  ap-computational-Id : {x y : A} → x ＝ʲ y → f x ＝ʲ f y
  ap-computational-Id =
    computational-eq-yoneda-eq ∘ ap-yoneda-Id f ∘ yoneda-eq-computational-eq

  compute-ap-refl-computational-Id :
    {x : A} →
    ap-computational-Id (reflʲ {x = x}) ＝ reflʲ
  compute-ap-refl-computational-Id = refl

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

  compute-ap-id-computational-Id :
    {x y : A} (p : x ＝ʲ y) → ap-computational-Id id p ＝ p
  compute-ap-id-computational-Id p =
    ( ap
      ( computational-eq-yoneda-eq)
      ( compute-ap-id-yoneda-Id (yoneda-eq-computational-eq p))) ∙
    ( is-section-yoneda-eq-computational-eq p)

Transport along computational identifications

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

  tr-computational-Id : {x y : A} → x ＝ʲ y → B x → B y
  tr-computational-Id = tr B ∘ eq-computational-eq

  compute-tr-refl-computational-Id :
    {x : A} → tr-computational-Id (reflʲ {x = x}) ＝ id
  compute-tr-refl-computational-Id = refl

Function extensionality with respect to computational identifications

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x}
  where

  htpy-computational-eq : f ＝ʲ g → f ~ g
  htpy-computational-eq = htpy-eq ∘ eq-computational-eq

  computational-eq-htpy : f ~ g → f ＝ʲ g
  computational-eq-htpy = computational-eq-eq ∘ eq-htpy

  equiv-htpy-computational-eq : (f ＝ʲ g) ≃ (f ~ g)
  equiv-htpy-computational-eq = equiv-funext ∘e equiv-eq-computational-eq

  equiv-computational-eq-htpy : (f ~ g) ≃ (f ＝ʲ g)
  equiv-computational-eq-htpy = equiv-computational-eq-eq ∘e equiv-eq-htpy

  funext-computational-Id : is-equiv htpy-computational-eq
  funext-computational-Id = is-equiv-map-equiv equiv-htpy-computational-eq

Univalence with respect to computational identifications

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

  map-computational-eq : A ＝ʲ B → A → B
  map-computational-eq = map-eq ∘ eq-computational-eq

  equiv-computational-eq : A ＝ʲ B → A ≃ B
  equiv-computational-eq = equiv-eq ∘ eq-computational-eq

  computational-eq-equiv : A ≃ B → A ＝ʲ B
  computational-eq-equiv = computational-eq-eq ∘ eq-equiv

  equiv-equiv-computational-eq : (A ＝ʲ B) ≃ (A ≃ B)
  equiv-equiv-computational-eq = equiv-univalence ∘e equiv-eq-computational-eq

  is-equiv-equiv-computational-eq : is-equiv equiv-computational-eq
  is-equiv-equiv-computational-eq =
    is-equiv-map-equiv equiv-equiv-computational-eq

  equiv-computational-eq-equiv : (A ≃ B) ≃ (A ＝ʲ B)
  equiv-computational-eq-equiv = equiv-computational-eq-eq ∘e equiv-eq-equiv A B

  is-equiv-computational-eq-equiv : is-equiv computational-eq-equiv
  is-equiv-computational-eq-equiv =
    is-equiv-map-equiv equiv-computational-eq-equiv

Recent changes

2024-02-19. Fredrik Bakke. Higher computational properties of computational identity types (#1026).
2024-02-08. Fredrik Bakke. Computational identity types (#1015).

agda-unimath