Identity type.

\begin{code}

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

module MLTT.Id where

open import MLTT.Universes
open import MLTT.Pi

open import MLTT.Identity-Type renaming (_๏ผ_ to infix 0 _๏ผ_) public

๐“ป๐“ฎ๐’ป๐“ต : {X : ๐“ค ฬ‡ } (x : X) โ†’ x ๏ผ x
๐“ป๐“ฎ๐’ป๐“ต x = refl {_} {_} {x}

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


private

 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

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

_โˆ™_ : {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

transportโปยน : {X : ๐“ค ฬ‡ } (A : X โ†’ ๐“ฅ ฬ‡ ) {x y : X} โ†’ x ๏ผ y โ†’ A y โ†’ A x
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}

Notations to make some proofs more readable:

\begin{code}

by-definition : {X : ๐“ค ฬ‡ } {x : X} โ†’ x ๏ผ x
by-definition = refl

by-construction : {X : ๐“ค ฬ‡ } {x : X} โ†’ x ๏ผ x
by-construction = refl

by-assumption : {X : ๐“ค ฬ‡ } {x : X} โ†’ x ๏ผ x
by-assumption = refl

\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  3  _โปยน
infix  1 _โˆŽ
infixr 0 _๏ผโŸจ_โŸฉ_
infixl 2 _โˆ™_
infix  4  _โˆผ_

\end{code}