# The strictly right unital concatenation operation on identifications

Content created by Fredrik Bakke, Egbert Rijke and maybemabeline.

Created on 2024-02-08.

module foundation.strictly-right-unital-concatenation-identifications where

Imports
open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.identity-types


## Idea

The concatenation operation on identifications is a family of binary operations

  _∙_ : x ＝ y → y ＝ z → x ＝ z


indexed by x y z : A. However, there are essentially three different ways we can define concatenation of identifications, all with different computational behaviours:

1. We can define concatenation by induction on the equality x ＝ y. This gives us the computation rule refl ∙ q ≐ q.
2. We can define concatenation by induction on the equality y ＝ z. This gives us the computation rule p ∙ refl ≐ p.
3. We can define concatenation by induction on both x ＝ y and y ＝ z. This only gives us the computation rule refl ∙ refl ≐ refl.

While the third option may be preferred by some for its symmetry, for practical reasons, we prefer one of the first two, and by convention we use the first alternative. However, there are cases where the second case may be preferred. Hence why we on this page consider the strictly right unital concatenation operation on identifications.

This definition is for instance used with the strictly involutive identity types to construct a strictly left unital concatenation operation.

## Definition

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

infixl 15 _∙ᵣ_
_∙ᵣ_ : {x y z : A} → x ＝ y → y ＝ z → x ＝ z
p ∙ᵣ refl = p

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

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


### Translating between the stictly left and stricly right unital versions of concatenation

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

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

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

eq-double-right-strict-concat-concat-left-associated :
{x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
(p ∙ q) ∙ r ＝ (p ∙ᵣ q) ∙ᵣ r
eq-double-right-strict-concat-concat-left-associated p q r =
( ap (_∙ r) (eq-right-strict-concat-concat p q)) ∙
( eq-right-strict-concat-concat (p ∙ᵣ q) r)

eq-double-right-strict-concat-concat-right-associated :
{x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
p ∙ (q ∙ r) ＝ p ∙ᵣ (q ∙ᵣ r)
eq-double-right-strict-concat-concat-right-associated p q r =
( ap (p ∙_) (eq-right-strict-concat-concat q r)) ∙
( eq-right-strict-concat-concat p (q ∙ᵣ r))

eq-double-concat-right-strict-concat-left-associated :
{x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
(p ∙ᵣ q) ∙ᵣ r ＝ (p ∙ q) ∙ r
eq-double-concat-right-strict-concat-left-associated p q r =
( ap (_∙ᵣ r) (eq-concat-right-strict-concat p q)) ∙
( eq-concat-right-strict-concat (p ∙ q) r)

eq-double-concat-right-strict-concat-right-associated :
{x y z w : A} (p : x ＝ y) (q : y ＝ z) (r : z ＝ w) →
p ∙ᵣ (q ∙ᵣ r) ＝ p ∙ (q ∙ r)
eq-double-concat-right-strict-concat-right-associated p q r =
( ap (p ∙ᵣ_) (eq-concat-right-strict-concat q r)) ∙
( eq-concat-right-strict-concat p (q ∙ r))


## Properties

### The groupoidal laws

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

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

left-unit-right-strict-concat : {x y : A} {p : x ＝ y} → refl ∙ᵣ p ＝ p
left-unit-right-strict-concat {p = refl} = refl

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

left-inv-right-strict-concat : {x y : A} (p : x ＝ y) → inv p ∙ᵣ p ＝ refl
left-inv-right-strict-concat refl = refl

right-inv-right-strict-concat : {x y : A} (p : x ＝ y) → p ∙ᵣ inv p ＝ refl
right-inv-right-strict-concat refl = refl

inv-inv-right-strict-concat : {x y : A} (p : x ＝ y) → inv (inv p) ＝ p
inv-inv-right-strict-concat refl = refl

distributive-inv-right-strict-concat :
{x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) →
inv (p ∙ᵣ q) ＝ inv q ∙ᵣ inv p
distributive-inv-right-strict-concat refl refl = refl


### Transposing inverses

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

left-transpose-eq-right-strict-concat :
{x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
p ∙ᵣ q ＝ r → q ＝ inv p ∙ᵣ r
left-transpose-eq-right-strict-concat refl q r s =
(inv left-unit-right-strict-concat ∙ s) ∙ inv left-unit-right-strict-concat

right-transpose-eq-right-strict-concat :
{x y : A} (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
p ∙ᵣ q ＝ r → p ＝ r ∙ᵣ inv q
right-transpose-eq-right-strict-concat p refl r s = s


### Concatenation is injective

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

is-injective-right-strict-concat :
{x y z : A} (p : x ＝ y) {q r : y ＝ z} → p ∙ᵣ q ＝ p ∙ᵣ r → q ＝ r
is-injective-right-strict-concat refl s =
(inv left-unit-right-strict-concat ∙ s) ∙ left-unit-right-strict-concat

is-injective-right-strict-concat' :
{x y z : A} (r : y ＝ z) {p q : x ＝ y} → p ∙ᵣ r ＝ q ∙ᵣ r → p ＝ q
is-injective-right-strict-concat' refl s = s