Chuangjie Xu 2013 (updated in February 2015)

This module makes use of Agda's irrelevant fields.

\begin{code}

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

module UsingIrrelevantFunext.Irrelevance where

open import Preliminaries.SetsAndFunctions
open import Preliminaries.NaturalNumber hiding (_+_)
open import Preliminaries.Boolean

record [_] {ℓ} (X : Set ℓ) : Set ℓ where
 constructor
   hide
 field 
  .reveal : X

open [_]

back-to-∅ : [ ∅ ] → ∅
back-to-∅ (hide ())

extension : {X Y : Set} → (X → [ Y ]) → [ X ] → [ Y ]
extension f (hide x) = hide (reveal (f x))

\end{code}

From now on, we only use [_], hide and the above extension operator to
define everything else, and so works for any monad:

\begin{code}

[∅]-elim : {A : Set} → [ ∅ ] → A
[∅]-elim = ∅-elim ∘ back-to-∅

functor : {X Y : Set} → (X → Y) → [ X ] → [ Y ]
functor f = extension (hide ∘ f)

functor₂ : {X Y Z : Set} → (X → Y → Z) → [ X ] → [ Y ] → [ Z ]
functor₂ f xh yh = extension(λ x → functor (f x) yh) xh

Lemma[[X→Y]⇒X→[Y]] : {X : Set}{Y : X → Set} → [ ((x : X) → Y x) ] → (x : X) → [ Y x ]
Lemma[[X→Y]⇒X→[Y]] fh x = functor(λ f → f x) fh

Lemma[[X→Y]⇒[X]→[Y]] : {X Y : Set} → [ (X → Y) ] → [ X ] → [ Y ]
Lemma[[X→Y]⇒[X]→[Y]] fh = extension(Lemma[[X→Y]⇒X→[Y]] fh)

decidable-structure : {X : Set} → decidable X → [ X ] → X
decidable-structure (inl x) xh = x
decidable-structure (inr u) xh = [∅]-elim (functor u xh)

Lemma[[≡]→≡]-ℕ : {m n : ℕ} → [ m ≡ n ] → m ≡ n
Lemma[[≡]→≡]-ℕ {m} {n} = decidable-structure (ℕ-discrete m n)

Lemma[[≡]→≡]-₂ : {b b' : ₂} → [ b ≡ b' ] → b ≡ b'
Lemma[[≡]→≡]-₂ {b} {b'} = decidable-structure (₂-discrete b b')

\end{code}

The double negations of identity type and related properties:

\begin{code}

[refl] : {X : Set}{x : X} → [ x ≡ x ]
[refl] = hide refl

[sym] : {X : Set}{x₀ x₁ : X} → [ x₀ ≡ x₁ ] → [ x₁ ≡ x₀ ]
[sym] = functor _⁻¹

[trans] : {X : Set}{x₀ x₁ x₂ : X} → [ x₀ ≡ x₁ ] → [ x₁ ≡ x₂ ] → [ x₀ ≡ x₂ ]
[trans] = functor₂ _·_

[transport] : {X : Set}{x x' : X}(Y : X → Set) → [ x ≡ x' ] → [ Y x ] → [ Y x' ]
[transport] Y = functor₂ (transport Y)

[ap] : {X Y : Set} → (f : X → Y) → {x₀ x₁ : X} → [ x₀ ≡ x₁ ] → [ f x₀ ≡ f x₁ ]
[ap] f = functor (ap f)

[fun-ap] : {X Y : Set} → ∀{f g : X → Y} → [ f ≡ g ] → ∀(x : X) → [ f x ≡ g x ]
[fun-ap] eh x = functor(λ e → fun-ap e x) eh

[pair⁼] : {X : Set}{Y : X → Set}{x x' : X}{y : Y x}{y' : Y x'}
        → (p : x ≡ x') → [ transport Y p y ≡ y' ] → [ (x , y) ≡ (x' , y') ]
[pair⁼] p = functor (pair⁼ p)

[pairˣ⁼] : {X Y : Set} {x x' : X} {y y' : Y}
         → [ x ≡ x' ] → [ y ≡ y' ] → [ (x , y) ≡ (x' , y') ]
[pairˣ⁼] = functor₂ pairˣ⁼

\end{code}