\begin{code} 

{-# OPTIONS --without-K #-}

module mini-library where

id : {X : Set}  X  X
id x = x

_∘_ : {X Y Z : Set}  (Y  Z)  (X  Y)  (X  Z)
g  f = λ x  g(f x)

infixl 30 _∘_ 

record Σ {I : Set} (X : I  Set) : Set where
  constructor _,_
  field
   i : I
   x : X i

π₀ : {I : Set} {X : I  Set}  (Σ \(i : I)  X i)  I
π₀(i , x) = i

π₁ : {I : Set} {X : I  Set}  (pair : Σ \(i : I)  X i)  X(π₀ pair)
π₁(i , x) = x

_×_ : Set  Set  Set
X × Y = Σ \(x : X)  Y

infixl 5 _,_ 
infixl 5 _×_ 
infixl 5 _⇔_

_⇔_ : Set  Set  Set
X  Y = (X  Y) × (Y  X)

data  : Set where

∅-elim : {X : Set}    X
∅-elim () 

data _+_ (X₀ X₁ : Set) : Set where
 in₀ : X₀  X₀ + X₁
 in₁ : X₁  X₀ + X₁

data _≡_ {X : Set} : X  X  Set where
  refl : {x : X}  x  x

J : {X : Set} (A : {x y : X}  x  y  Set)
    ({x : X}  A (refl {X} {x}))  {x y : X} (p : x  y)  A p
J A φ refl = φ

\end{code}

The version of J introduced by Paulin-Mohring can be defined using J,
as is well known, but we define using pattern matching for simplicity:

\begin{code} 

J' : {X : Set} (x : X)  (A : {y : X}  x  y  Set)
    A (refl {X} {x})  {y : X} (p : x  y)  A p
J' x A φ refl = φ

weak-J : {X : Set} (B : (x y : X)  Set) 
  ({x : X}  B x x)  {x y : X}  x  y  B x y
weak-J {X} B = J A
 where
  A : {x y : X}  x  y  Set
  A {x} {y} p = B x y

trans : {X : Set}  {x y z : X}  x  y  y  z  x  z
trans {X} {x} {y} {z} r = weak-J  x y  (z : X)  y  z  x  z)  z s  s) r z

sym : {X : Set}  {x y : X}  x  y  y  x
sym {X} {x} {y} = weak-J  x y  y  x) refl 

cong : {X Y : Set}  (f : X  Y)  {x x' : X}  x  x'  f x  f x'
cong {X} {Y} f = weak-J x x'  f x  f x') refl

subst : {X : Set} {P : X  Set}  {x y : X}  x  y  P x  P y
subst {X} {P} = weak-J  x y  P x  P y)  p  p)

\end{code}

The above is the traditional notation. The homotopy theory notation is
this:

\begin{code} 

_•_ : {X : Set}  {x y z : X}  x  y  y  z  x  z
p  q = trans p q

_⁻¹ : {X : Set}  {x y : X}  x  y  y  x
p ⁻¹ = sym p

infixr 6 _≡_
infixr 7 _•_

\end{code}

Some very simple lemmas:

\begin{code} 

sym-is-inverse : {X : Set} {x y : X} (p : x  y)  refl  p ⁻¹  p
sym-is-inverse = J  p  refl  (p ⁻¹)  p) refl

sym-sym-trivial : {X : Set} {x y : X} (p : x  y)  p  (p ⁻¹)⁻¹
sym-sym-trivial = J  p  p  (p ⁻¹)⁻¹) refl

refl-is-right-id : {X : Set} {x y : X} (p : x  y)  p  p  refl
refl-is-right-id = J  q  q  q  refl) refl

refl-is-left-id : {X : Set} {x y : X} (p : x  y)  p  refl  p
refl-is-left-id = J  q  q  refl  q) refl

cong-id-is-id : {X : Set} {x y : X} (p : x  y)  p  cong id p
cong-id-is-id = J  p  p  cong id p) refl

\end{code}

The following is quite involved without pattern matching; see
Nils Anders Danielsson's Agda library.

\begin{code} 

split : {X : Set} {Y : X  Set} (x x' : X) (y : Y x) (y' : Y x')
      (p : x  x')  subst p y  y'  _≡_ {Σ \x  Y x} (x , y) (x' , y') 
split .x' x' .y y refl refl = refl

\end{code}

This notational trick is also from Nils Anders Danielsson. 

\begin{code} 

infix  0 finally
infixr 0 _≡⟨_⟩_

_≡⟨_⟩_ : {A : Set} (x : A) {y z : A}  x  y  y  z  x  z
_ ≡⟨ p  q = p  q

finally : {A : Set} (x y : A)  x  y  x  y
finally _ _ p = p

syntax finally x y p = x ≡⟨ p ⟩∎ y ∎

\end{code}

Two more simple lemmas:

\begin{code} 

sym-trans : {X : Set} {x y z : X} (p : x  y) (q : y  z)  (q ⁻¹)  (p ⁻¹)  (p  q)⁻¹
sym-trans {X} {x} {y} {z} p = J' y   q  (q ⁻¹)  (p ⁻¹)  (p  q)⁻¹) trivial
   where 
    trivial : refl  (p ⁻¹)  (p  refl)⁻¹
    trivial = refl  (p ⁻¹) ≡⟨ (refl-is-left-id (p ⁻¹))⁻¹ 
              p ⁻¹          ≡⟨ cong sym (refl-is-right-id p) ⟩∎
              (p  refl)⁻¹  

trans-assoc : {X : Set} {x y z w : X} (p : x  y) (q : y  z) (r : z  w)  (p  q)  r  p  (q  r)
trans-assoc {X} {x} {y} {z} {w} p q = J' z  r  (p  q)  r  p  (q  r)) (trivial ⁻¹)
   where 
    trivial = p  (q  refl) ≡⟨ cong  q  p  q) ((refl-is-right-id q)⁻¹) 
              p  q          ≡⟨ refl-is-right-id _ ⟩∎
              (p  q)  refl 

\end{code}

\begin{code} 

data  : Set where
  : 
  : 

\end{code}