Identity type.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module Id where

open import Universes
open import Pi

data _≑_ {𝓀} {X : 𝓀 Μ‡ } : X β†’ X β†’ 𝓀 Μ‡  where
  refl : {x : X} β†’ x ≑ x

refl─ : {X : 𝓀 Μ‡ } (x : X) β†’ x ≑ x
refl─ x = refl

lhs : {X : 𝓀 Μ‡ } {x y : X} β†’ x ≑ y β†’ X
lhs {𝓀} {X} {x} {y} p = x

rhs : {X : 𝓀 Μ‡ } {x y : X} β†’ x ≑ y β†’ X
rhs {𝓀} {X} {x} {y} p = y

Id : {X : 𝓀 Μ‡ } β†’ X β†’ X β†’ 𝓀 Μ‡
Id = _≑_

Jbased : {X : 𝓀 Μ‡ } (x : X) (A : (y : X) β†’ x ≑ y β†’ π“₯ Μ‡ )
       β†’ A x refl β†’ (y : X) (r : x ≑ y) β†’ A y r
Jbased x A b .x refl = b

J : {X : 𝓀 Μ‡ } (A : (x y : X) β†’ x ≑ y β†’ π“₯ Μ‡ )
  β†’ ((x : X) β†’ A x x refl) β†’ {x y : X} (r : x ≑ y) β†’ A x y r
J A f {x} {y} = Jbased x (A x) (f x) y

transport' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X}
          β†’ x ≑ y β†’ A x β†’ A y
transport' A {x} {y} p a = Jbased x (Ξ» y p β†’ A y) a y p

transport : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X}
          β†’ x ≑ y β†’ A x β†’ A y
transport A refl = id

_βˆ™_ : {X : 𝓀 Μ‡ } {x y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
p βˆ™ q = transport (lhs p ≑_) q p

_⁻¹ : {X : 𝓀 Μ‡ } β†’ {x y : X} β†’ x ≑ y β†’ y ≑ x
p ⁻¹ = transport (_≑ lhs p) p refl

ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x x' : X} β†’ x ≑ x' β†’ f x ≑ f x'
ap f p = transport (Ξ» - β†’ f (lhs p) ≑ f -) p refl

back-transport : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y : X} β†’ x ≑ y β†’ A y β†’ A x
back-transport B p = transport B (p ⁻¹)

_∼_ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } β†’ ((x : X) β†’ A x) β†’ ((x : X) β†’ A x) β†’ 𝓀 βŠ” π“₯ Μ‡
f ∼ g = βˆ€ x β†’ f x ≑ g x

\end{code}

Standard syntax for equality chain reasoning:

\begin{code}

_β‰‘βŸ¨_⟩_ : {X : 𝓀 Μ‡ } (x : X) {y z : X} β†’ x ≑ y β†’ y ≑ z β†’ x ≑ z
_ β‰‘βŸ¨ p ⟩ q = p βˆ™ q

_∎ : {X : 𝓀 Μ‡ } (x : X) β†’ x ≑ x
_∎ _ = refl

\end{code}

Fixities:

\begin{code}

infix  0 _≑_
infix  3  _⁻¹
infix  1 _∎
infixr 0 _β‰‘βŸ¨_⟩_
infixl 2 _βˆ™_
infix  4  _∼_

\end{code}