# Strictly involutive identity types

Content created by Fredrik Bakke.

Created on 2024-02-08.
Last modified on 2024-03-12.

module foundation.strictly-involutive-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.multivariable-homotopies
open import foundation.strictly-right-unital-concatenation-identifications
open import foundation.univalence
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

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
open import foundation-core.transport-along-identifications


## 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 strictly involutive identity types

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


whose elements we call strictly involutive identifications. This type family is equivalent to the standard identity types, but satisfies the strict laws

• invⁱ (invⁱ p) ≐ p
• invⁱ reflⁱ ≐ reflⁱ

where we use a superscript i to distinguish the strictly involutive identity type from the standard identity type.

In addition, we maintain the following strict laws

• invⁱ reflⁱ ≐ reflⁱ
• reflⁱ ∙ p ≐ p or p ∙ reflⁱ ≐ p
• ind-Idⁱ B f reflⁱ ≐ f reflⁱ

among other more specific laws considered on this page.

## Definition

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

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

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

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


## Properties

### The strictly involutive identity types are equivalent to the standard identity types

The equivalence (x ＝ y) ≃ (x ＝ⁱ y) is defined from left to right by inclusion at the second component

  involutive-eq-eq := p ↦ (x , p , refl)   : x ＝ y → x ＝ⁱ y,


and from right to left by the concatenation

  eq-involutive-eq := (z , p , q) ↦ inv q ∙ p   : x ＝ⁱ y → x ＝ y.


This equivalence weakly preserves the groupoid structure on the strictly involutive identity types as we will see later. Moreover, the composition eq-involutive-eq ∘ involutive-eq-eq computes strictly to the identity:

  eq-involutive-eq ∘ involutive-eq-eq
≐ p ↦ (((z , p , q) ↦ inv q ∙ p) (r ↦ (w , r , refl)))
≐ p ↦ inv refl ∙ p
≐ p ↦ refl ∙ p
≐ p ↦ p


and the reflexivities are preserved strictly:

  eq-involutive-eq reflⁱ ≐ inv refl ∙ refl ≐ refl ∙ refl ≐ refl,


and

  involutive-eq-eq refl ≐ (x , refl , refl) ≐ reflⁱ.

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

involutive-eq-eq : x ＝ y → x ＝ⁱ y
involutive-eq-eq p = (x , p , refl)

eq-involutive-eq : x ＝ⁱ y → x ＝ y
eq-involutive-eq (z , p , q) = inv q ∙ p

is-section-eq-involutive-eq : is-section involutive-eq-eq eq-involutive-eq
is-section-eq-involutive-eq (z , p , refl) = refl

is-retraction-eq-involutive-eq :
is-retraction involutive-eq-eq eq-involutive-eq
is-retraction-eq-involutive-eq p = refl

is-equiv-involutive-eq-eq : is-equiv involutive-eq-eq
pr1 (pr1 is-equiv-involutive-eq-eq) = eq-involutive-eq
pr2 (pr1 is-equiv-involutive-eq-eq) = is-section-eq-involutive-eq
pr1 (pr2 is-equiv-involutive-eq-eq) = eq-involutive-eq
pr2 (pr2 is-equiv-involutive-eq-eq) = is-retraction-eq-involutive-eq

is-equiv-eq-involutive-eq : is-equiv eq-involutive-eq
pr1 (pr1 is-equiv-eq-involutive-eq) = involutive-eq-eq
pr2 (pr1 is-equiv-eq-involutive-eq) = is-retraction-eq-involutive-eq
pr1 (pr2 is-equiv-eq-involutive-eq) = involutive-eq-eq
pr2 (pr2 is-equiv-eq-involutive-eq) = is-section-eq-involutive-eq

equiv-involutive-eq-eq : (x ＝ y) ≃ (x ＝ⁱ y)
pr1 equiv-involutive-eq-eq = involutive-eq-eq
pr2 equiv-involutive-eq-eq = is-equiv-involutive-eq-eq

equiv-eq-involutive-eq : (x ＝ⁱ y) ≃ (x ＝ y)
pr1 equiv-eq-involutive-eq = eq-involutive-eq
pr2 equiv-eq-involutive-eq = is-equiv-eq-involutive-eq


This equivalence preserves the reflexivity elements strictly in both directions.

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

preserves-refl-involutive-eq-eq :
{x : A} → involutive-eq-eq (refl {x = x}) ＝ reflⁱ
preserves-refl-involutive-eq-eq = refl

preserves-refl-eq-involutive-eq :
{x : A} → eq-involutive-eq (reflⁱ {x = x}) ＝ refl
preserves-refl-eq-involutive-eq = refl


### Torsoriality of the strictly involutive identity types

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

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


### The dependent universal property of the strictly involutive identity types

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

dependent-universal-property-identity-system-involutive-Id :
dependent-universal-property-identity-system
( involutive-Id x)
( reflⁱ)
dependent-universal-property-identity-system-involutive-Id =
dependent-universal-property-identity-system-is-torsorial
( reflⁱ)
( is-torsorial-involutive-Id)


### The induction principle for strictly involutive identity types

The strictly involutive 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ⁱ. The strictly involutive identity types also satisfy the corresponding computation rule strictly.

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

ind-involutive-Id :
B x reflⁱ → (y : A) (p : x ＝ⁱ y) → B y p
ind-involutive-Id b .x (.x , refl , refl) = b

compute-ind-involutive-Id :
(b : B x reflⁱ) → ind-involutive-Id b x reflⁱ ＝ b
compute-ind-involutive-Id b = refl

uniqueness-ind-involutive-Id :
(f : (y : A) (p : x ＝ⁱ y) → B y p) →
ind-involutive-Id (f x reflⁱ) ＝ f
uniqueness-ind-involutive-Id f =
eq-multivariable-htpy 2 (λ where .x (.x , refl , refl) → refl)


Note. The only reason we must apply function extensionality is to show uniqueness of the induction principle up to equality.

## Structure

The strictly involutive identity types form a strictly involutive weak groupoidal structure on types.

### Inverting strictly involutive identifications

We have an inversion operation on involutive-Id defined by swapping the position of the identifications. This operation satisfies the strict laws

• invⁱ (invⁱ p) ≐ p, and
• invⁱ reflⁱ ≐ reflⁱ.
module _
{l : Level} {A : UU l}
where

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

compute-refl-inv-involutive-Id : {x : A} → invⁱ (reflⁱ {x = x}) ＝ reflⁱ
compute-refl-inv-involutive-Id = refl

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


The inversion operation corresponds to the standard inversion operation on identifications.

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

preserves-inv-involutive-eq-eq :
{x y : A} (p : x ＝ y) →
involutive-eq-eq (inv p) ＝ invⁱ (involutive-eq-eq p)
preserves-inv-involutive-eq-eq refl = refl

preserves-inv-eq-involutive-eq :
{x y : A} (p : x ＝ⁱ y) →
eq-involutive-eq (invⁱ p) ＝ inv (eq-involutive-eq p)
preserves-inv-eq-involutive-eq (z , p , q) =
ap (inv p ∙_) (inv (inv-inv q)) ∙ inv (distributive-inv-concat (inv q) p)


### Concatenation of strictly involutive identifications

We have, practically speaking, two definitions of the concatenation operation on strictly involutive identity types. One satisfies a strict left unit law and the other satisfies a strict right unit law. In both cases, we must use the strictly right unital concatenation operation on standard identifications _∙ᵣ_, to obtain this strict one-sided unit law, as will momentarily be demonstrated.

The strictly left unital concatenation operation is defined by

  (w , p , q) ∙ⁱ (w' , p' , q') := (w' , p' , (q' ∙ᵣ inv p) ∙ᵣ q),


and the strictly right unital concatenation operation is defined by

  (w , p , q) ∙ᵣⁱ (w' , p' , q') = (w , (p ∙ᵣ inv q') ∙ᵣ p' , q).


The following computation verifies that the strictly left unital concatenation operation is indeed strictly left unital:

  reflⁱ ∙ⁱ r
≐ (x , refl , refl) ∙ⁱ (w , p , q)
≐ (w , p , (q ∙ᵣ inv refl) ∙ᵣ refl)
≐ (w , p , (q ∙ᵣ inv refl))
≐ (w , p , (q ∙ᵣ refl))
≐ (w , p , q)
≐ r.


While for the strictly right unital concatenation operation, we have the computation

  r ∙ᵣⁱ reflⁱ
≐  (w , p , q) ∙ᵣⁱ (x , refl , refl)
≐ (w , (p ∙ᵣ inv refl) ∙ᵣ refl , q)
≐ (w , p ∙ᵣ inv refl , q)
≐ (w , p ∙ᵣ refl , q)
≐ (w , p , q)
≐ r.


To be consistent with the convention for the standard identity types, we take the strictly left unital concatenation operation to be the default concatenation operation on strictly involutive identity types.

#### The strictly left 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' , (q' ∙ᵣ inv p) ∙ᵣ q)

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

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

preserves-concat-involutive-eq-eq :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
involutive-eq-eq (p ∙ q) ＝ involutive-eq-eq p ∙ⁱ involutive-eq-eq q
preserves-concat-involutive-eq-eq refl q = refl

preserves-concat-eq-involutive-eq :
{x y z : A} (p : x ＝ⁱ y) (q : y ＝ⁱ z) →
eq-involutive-eq (p ∙ⁱ q) ＝ eq-involutive-eq p ∙ eq-involutive-eq q
preserves-concat-eq-involutive-eq (w , p , q) (w' , p' , q') =
( ap
( _∙ p')
( ( distributive-inv-right-strict-concat (q' ∙ᵣ inv p) q) ∙
( ( ap
( inv q ∙ᵣ_)
( ( distributive-inv-right-strict-concat q' (inv p)) ∙
( ap (_∙ᵣ inv q') (inv-inv p)))) ∙
( inv (assoc-right-strict-concat (inv q) p (inv q'))) ∙
( eq-double-concat-right-strict-concat-left-associated
( inv q)
( p)
( inv q'))))) ∙
( assoc (inv q ∙ p) (inv q') p')


#### 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-involutive-Id :
{x y : A} → x ＝ⁱ y → (z : A) → y ＝ⁱ z → x ＝ⁱ z
right-strict-concat-involutive-Id p z q = p ∙ᵣⁱ q

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

eq-concat-right-strict-concat-involutive-Id :
{x y z : A} (p : x ＝ⁱ y) (q : y ＝ⁱ z) → p ∙ᵣⁱ q ＝ p ∙ⁱ q
eq-concat-right-strict-concat-involutive-Id (w , refl , q) (w' , p' , refl) =
eq-pair-eq-fiber
( eq-pair
( left-unit-right-strict-concat)
( inv left-unit-right-strict-concat))

preserves-right-strict-concat-involutive-eq-eq :
{x y z : A} (p : x ＝ y) (q : y ＝ z) →
involutive-eq-eq (p ∙ q) ＝ involutive-eq-eq p ∙ᵣⁱ involutive-eq-eq q
preserves-right-strict-concat-involutive-eq-eq p refl =
ap involutive-eq-eq right-unit

preserves-right-strict-concat-eq-involutive-eq :
{x y z : A} (p : x ＝ⁱ y) (q : y ＝ⁱ z) →
eq-involutive-eq (p ∙ᵣⁱ q) ＝ eq-involutive-eq p ∙ eq-involutive-eq q
preserves-right-strict-concat-eq-involutive-eq (w , p , q) (w' , p' , q') =
( ap
( inv q ∙_)
( ( eq-double-concat-right-strict-concat-left-associated p (inv q') p') ∙
( assoc p (inv q') p'))) ∙
( inv (assoc (inv q) p (inv q' ∙ p')))


### The groupoidal laws for the strictly involutive identity types

The general proof strategy is to induct on the minimal number of identifications to make the left endpoints strictly equal, and then proceed by reasoning with the groupoid laws of the underlying identity types.

#### The groupoidal laws for the strictly left unital concatenation operation

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

assoc-involutive-Id :
(p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) → (p ∙ⁱ q) ∙ⁱ r ＝ p ∙ⁱ (q ∙ⁱ r)
assoc-involutive-Id (_ , p , q) (_ , p' , q') (_ , p'' , q'') =
eq-pair-eq-fiber
( eq-pair-eq-fiber
( ( inv (assoc-right-strict-concat (q'' ∙ᵣ inv p') (q' ∙ᵣ inv p) q)) ∙
( ap
( _∙ᵣ q)
( inv (assoc-right-strict-concat (q'' ∙ᵣ inv p') q' (inv p))))))


Note. Observe that the previous proof relies solely on the associator of the underlying identity type. This is one of the fundamental observations leading to the construction of the computational identity type.

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

left-unit-involutive-Id :
{p : x ＝ⁱ y} → reflⁱ ∙ⁱ p ＝ p
left-unit-involutive-Id = refl

right-unit-involutive-Id :
{p : x ＝ⁱ y} → p ∙ⁱ reflⁱ ＝ p
right-unit-involutive-Id {p = .y , refl , q} =
eq-pair-eq-fiber (eq-pair-eq-fiber left-unit-right-strict-concat)

left-inv-involutive-Id :
(p : x ＝ⁱ y) → invⁱ p ∙ⁱ p ＝ reflⁱ
left-inv-involutive-Id (.y , refl , q) =
eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-right-strict-concat q))

right-inv-involutive-Id :
(p : x ＝ⁱ y) → p ∙ⁱ invⁱ p ＝ reflⁱ
right-inv-involutive-Id (.x , p , refl) =
eq-pair-eq-fiber (eq-pair-eq-fiber (right-inv-right-strict-concat p))

distributive-inv-concat-involutive-Id :
(p : x ＝ⁱ y) {z : A} (q : y ＝ⁱ z) → invⁱ (p ∙ⁱ q) ＝ invⁱ q ∙ⁱ invⁱ p
distributive-inv-concat-involutive-Id (.y , refl , q') (.y , p' , refl) =
eq-pair-eq-fiber
( eq-pair
( left-unit-right-strict-concat)
( inv left-unit-right-strict-concat))


#### The groupoidal laws for the strictly right unital concatenation operation

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

assoc-right-strict-concat-involutive-Id :
(p : x ＝ⁱ y) (q : y ＝ⁱ z) (r : z ＝ⁱ w) → (p ∙ᵣⁱ q) ∙ᵣⁱ r ＝ p ∙ᵣⁱ (q ∙ᵣⁱ r)
assoc-right-strict-concat-involutive-Id
( _ , p , q) (_ , p' , q') (_ , p'' , q'') =
eq-pair-eq-fiber
( eq-pair
( ( assoc-right-strict-concat (p ∙ᵣ inv q' ∙ᵣ p') (inv q'') p'') ∙
( assoc-right-strict-concat (p ∙ᵣ inv q') p' (inv q'' ∙ᵣ p'')) ∙
( ap
( p ∙ᵣ inv q' ∙ᵣ_)
( inv (assoc-right-strict-concat p' (inv q'') p''))))
( refl))

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

left-unit-right-strict-concat-involutive-Id :
{p : x ＝ⁱ y} → reflⁱ ∙ᵣⁱ p ＝ p
left-unit-right-strict-concat-involutive-Id {p = .x , p , refl} =
eq-pair-eq-fiber (eq-pair left-unit-right-strict-concat refl)

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

left-inv-right-strict-concat-involutive-Id :
(p : x ＝ⁱ y) → invⁱ p ∙ᵣⁱ p ＝ reflⁱ
left-inv-right-strict-concat-involutive-Id (.y , refl , q) =
eq-pair-eq-fiber (eq-pair (right-inv-right-strict-concat q) refl)

right-inv-right-strict-concat-involutive-Id :
(p : x ＝ⁱ y) → p ∙ᵣⁱ invⁱ p ＝ reflⁱ
right-inv-right-strict-concat-involutive-Id (.x , p , refl) =
eq-pair-eq-fiber (eq-pair (right-inv-right-strict-concat p) refl)

distributive-inv-right-strict-concat-involutive-Id :
(p : x ＝ⁱ y) {z : A} (q : y ＝ⁱ z) →
invⁱ (p ∙ᵣⁱ q) ＝ invⁱ q ∙ᵣⁱ invⁱ p
distributive-inv-right-strict-concat-involutive-Id
( .y , refl , q) (.y , p' , refl) =
eq-pair-eq-fiber
( eq-pair
( inv left-unit-right-strict-concat)
( left-unit-right-strict-concat))


## Operations

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

### Action of functions on strictly involutive identifications

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

eq-ap-involutive-Id : {x y : A} → x ＝ⁱ y → f x ＝ f y
eq-ap-involutive-Id = ap f ∘ eq-involutive-eq

ap-involutive-Id : {x y : A} → x ＝ⁱ y → f x ＝ⁱ f y
ap-involutive-Id = involutive-eq-eq ∘ eq-ap-involutive-Id

compute-ap-refl-involutive-Id :
{x : A} → ap-involutive-Id (reflⁱ {x = x}) ＝ reflⁱ
compute-ap-refl-involutive-Id = refl

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

compute-ap-id-involutive-Id :
{x y : A} (p : x ＝ⁱ y) → ap-involutive-Id id p ＝ p
compute-ap-id-involutive-Id (z , q , refl) =
eq-pair-eq-fiber (eq-pair (ap-id q) refl)


### Action of binary functions on strictly involutive identifications

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

ap-binary-involutive-Id :
{x x' : A} (p : x ＝ⁱ x') {y y' : B} (q : y ＝ⁱ y') → f x y ＝ⁱ f x' y'
ap-binary-involutive-Id (z , p1 , p2) (w , q1 , q2) =
( f z w , ap-binary f p1 q1 , ap-binary f p2 q2)

left-unit-ap-binary-involutive-Id :
{x : A} {y y' : B} (q : y ＝ⁱ y') →
ap-binary-involutive-Id reflⁱ q ＝ ap-involutive-Id (f x) q
left-unit-ap-binary-involutive-Id (z , p , refl) = refl

right-unit-ap-binary-involutive-Id :
{x x' : A} (p : x ＝ⁱ x') {y : B} →
ap-binary-involutive-Id p reflⁱ ＝ ap-involutive-Id (λ z → f z y) p
right-unit-ap-binary-involutive-Id {.z} {x'} (z , p , refl) {y} =
eq-pair-eq-fiber (eq-pair right-unit refl)


### Transport along strictly involutive identifications

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

tr-involutive-Id : {x y : A} → x ＝ⁱ y → B x → B y
tr-involutive-Id = tr B ∘ eq-involutive-eq

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


### Function extensionality with respect to strictly involutive identifications

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

htpy-involutive-eq : f ＝ⁱ g → f ~ g
htpy-involutive-eq = htpy-eq ∘ eq-involutive-eq

involutive-eq-htpy : f ~ g → f ＝ⁱ g
involutive-eq-htpy = involutive-eq-eq ∘ eq-htpy

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

equiv-involutive-eq-htpy : (f ~ g) ≃ (f ＝ⁱ g)
equiv-involutive-eq-htpy = equiv-involutive-eq-eq ∘e equiv-eq-htpy

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

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

involutive-htpy-involutive-eq : f ＝ⁱ g → (x : A) → f x ＝ⁱ g x
involutive-htpy-involutive-eq (h , p , q) x =
( h x , htpy-eq p x , htpy-eq q x)

involutive-eq-involutive-htpy : ((x : A) → f x ＝ⁱ g x) → f ＝ⁱ g
involutive-eq-involutive-htpy H =
( pr1 ∘ H , eq-htpy (pr1 ∘ (pr2 ∘ H)) , eq-htpy (pr2 ∘ (pr2 ∘ H)))


It remains to show that these maps are part of an equivalence.

### Standard univalence with respect to strictly involutive identifications

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

map-involutive-eq : A ＝ⁱ B → A → B
map-involutive-eq = map-eq ∘ eq-involutive-eq

equiv-involutive-eq : A ＝ⁱ B → A ≃ B
equiv-involutive-eq = equiv-eq ∘ eq-involutive-eq

involutive-eq-equiv : A ≃ B → A ＝ⁱ B
involutive-eq-equiv = involutive-eq-eq ∘ eq-equiv

equiv-equiv-involutive-eq : (A ＝ⁱ B) ≃ (A ≃ B)
equiv-equiv-involutive-eq = equiv-univalence ∘e equiv-eq-involutive-eq

is-equiv-equiv-involutive-eq : is-equiv equiv-involutive-eq
is-equiv-equiv-involutive-eq = is-equiv-map-equiv equiv-equiv-involutive-eq

equiv-involutive-eq-equiv : (A ≃ B) ≃ (A ＝ⁱ B)
equiv-involutive-eq-equiv = equiv-involutive-eq-eq ∘e equiv-eq-equiv A B

is-equiv-involutive-eq-equiv : is-equiv involutive-eq-equiv
is-equiv-involutive-eq-equiv = is-equiv-map-equiv equiv-involutive-eq-equiv


### Whiskering of strictly involutive identifications

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

left-whisker-concat-involutive-Id :
(p : x ＝ⁱ y) {q r : y ＝ⁱ z} → q ＝ⁱ r → p ∙ⁱ q ＝ⁱ p ∙ⁱ r
left-whisker-concat-involutive-Id p β = ap-involutive-Id (p ∙ⁱ_) β

right-whisker-concat-involutive-Id :
{p q : x ＝ⁱ y} → p ＝ⁱ q → (r : y ＝ⁱ z) → p ∙ⁱ r ＝ⁱ q ∙ⁱ r
right-whisker-concat-involutive-Id α r = ap-involutive-Id (_∙ⁱ r) α


### Horizontal concatenation of strictly involutive identifications

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

horizontal-concat-involutive-Id² :
{p q : x ＝ⁱ y} → p ＝ⁱ q → {u v : y ＝ⁱ z} → u ＝ⁱ v → p ∙ⁱ u ＝ⁱ q ∙ⁱ v
horizontal-concat-involutive-Id² = ap-binary-involutive-Id (_∙ⁱ_)


### Vertical concatenation of strictly involutive identifications

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

vertical-concat-involutive-Id² :
{p q r : x ＝ⁱ y} → p ＝ⁱ q → q ＝ⁱ r → p ＝ⁱ r
vertical-concat-involutive-Id² α β = α ∙ⁱ β


## References

[Esc19]
Martín Hötzel Escardó. Definitions of equivalence satisfying judgmental/strict groupoid laws? Google groups forum discussion, 09 2019. URL: https://groups.google.com/g/homotopytypetheory/c/FfiZj1vrkmQ/m/GJETdy0AAgAJ.