------------------------------------------------------------------------
-- The "interval"
------------------------------------------------------------------------

-- Note that this module is experimental: it uses rewrite rules and
-- postulates to encode a higher inductive type.

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

-- Partly based on the HoTT book.

module Interval where

open import Equality.Propositional as Eq hiding (elim)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Equivalence equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J using (ext⁻¹)

------------------------------------------------------------------------
-- The interval

postulate

  -- The interval type constructor.

  I : Set

  -- Constructors.

  [0] [1] : I
  0≡1     : [0]  [1]

-- Eliminator.

module _ {p}
         (P : I  Set p)
         (p₀ : P [0])
         (p₁ : P [1])
         (p₀≡p₁ : subst P 0≡1 p₀  p₁)
         where

  postulate

    elim : (x : I)  P x

    -- Computation rules.
    --
    -- NOTE: Rewriting has not been activated for the "computation" rule
    -- corresponding to 0≡1.

    elim-[0] : elim [0]  p₀
    elim-[1] : elim [1]  p₁

  {-# REWRITE elim-[0] #-}
  {-# REWRITE elim-[1] #-}

  postulate

    elim-0≡1 : dependent-cong elim 0≡1  p₀≡p₁

------------------------------------------------------------------------
-- Non-dependent eliminator

-- A non-dependent eliminator.

rec :  {p} {P : Set p}
      (p₀ p₁ : P)
      (p₀≡p₁ : p₀  p₁) 
      I  P
rec p₀ p₁ p₀≡p₁ =
  elim _ p₀ p₁ (
    subst (const _) 0≡1 p₀  ≡⟨ subst-const 0≡1 
    p₀                      ≡⟨ p₀≡p₁ ⟩∎
    p₁                      )

-- A "computation rule" for rec.

rec-0≡1 :
   {p} {P : Set p}
  (p₀ p₁ : P)
  (p₀≡p₁ : p₀  p₁) 
  cong (rec p₀ p₁ p₀≡p₁) 0≡1  p₀≡p₁
rec-0≡1 p₀ p₁ p₀≡p₁ =
  cong (rec p₀ p₁ p₀≡p₁) 0≡1                                             ≡⟨⟩

  cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1                ≡⟨ sym $ trans-sym-[trans] _ _ 

  trans (sym $ subst-const 0≡1)
    (trans (subst-const 0≡1)
           (cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1))    ≡⟨ cong (trans _) $ sym $ dependent-cong-subst-const-cong _ 0≡1 

  trans (sym $ subst-const 0≡1)
    (dependent-cong (elim _ p₀ p₁ (trans (subst-const 0≡1) p₀≡p₁)) 0≡1)  ≡⟨ cong (trans _) $ elim-0≡1 _ _ _ _ 

  trans (sym $ subst-const 0≡1) (trans (subst-const 0≡1) p₀≡p₁)          ≡⟨ trans-sym-[trans] _ _ ⟩∎

  p₀≡p₁                                                                  

------------------------------------------------------------------------
-- Contractibility

-- The interval is contractible.

interval-contractible : Contractible I
interval-contractible = [1] , sym  f
  where
  f : (x : I)  x  [1]
  f = elim (_≡ [1]) 0≡1 refl
        (subst (_≡ [1]) 0≡1 0≡1              ≡⟨ cong  p  subst (_≡ [1]) p 0≡1)
                                                     (sym $ sym-sym 0≡1) 
         subst (_≡ [1]) (sym (sym 0≡1)) 0≡1  ≡⟨ subst-trans (sym 0≡1) 
         trans (sym 0≡1) 0≡1                 ≡⟨ trans-symˡ 0≡1 ⟩∎
         refl                                )

-- A simplification lemma for rec p p.

rec-const :
   {p} {P : Set p} (p : P) (p≡p : p  p) i 
  rec p p p≡p i  p
rec-const p p≡p i =
  rec p p p≡p i    ≡⟨ cong (rec p p p≡p) (_⇔_.to propositional⇔irrelevant (mono₁ 0 interval-contractible) i [0]) ⟩∎
  rec p p p≡p [0]  

------------------------------------------------------------------------
-- Extensionality

abstract

  -- The interval can be used to prove that equality of functions is
  -- extensional.

  private

    -- ext-helper {f = f} {g = g} f≡g reduces to λ x → f x when the
    -- input is [0], and to λ x → g x when the input is [1].

    ext-helper :
       {a b} {A : Set a} {B : A  Set b} {f g : (x : A)  B x} 
      (∀ x  f x  g x)  I  (x : A)  B x
    ext-helper {f = f} {g} f≡g i =
      λ x  rec (f x) (g x) (f≡g x) i

    ext′ :  {a b}  Extensionality a b
    ext′ {f = f} {g = g} f≡g =
      f                   ≡⟨⟩
      ext-helper f≡g [0]  ≡⟨ cong (ext-helper f≡g) 0≡1 ⟩∎
      ext-helper f≡g [1]  

  ext :  {a b}  Extensionality a b
  ext = good-ext ext′

  -- The function ext is an equivalence.

  ext-is-equivalence :
     {a b} {A : Set a} {B : A  Set b} {f g : (x : A)  B x} 
    Is-equivalence {A =  x  f x  g x} ext
  ext-is-equivalence = good-ext-is-equivalence ext′

  -- Equality rearrangement lemmas for ext.

  ext-refl :
     {a b} {A : Set a} {B : A  Set b} (f : (x : A)  B x) 
    ext  x  refl {x = f x})  refl {x = f}
  ext-refl = good-ext-refl ext′

  cong-ext :
     {a b} {A : Set a} {B : A  Set b} {f g : (x : A)  B x}
    (f≡g :  x  f x  g x) {x} 
    cong (_$ x) (ext f≡g)  f≡g x
  cong-ext = cong-good-ext ext′

  subst-ext :
     {a b p} {A : Set a} {B : A  Set b} {f g : (x : A)  B x} {x}
    (P : B x  Set p) {p} (f≡g :  x  f x  g x) 
    subst  f  P (f x)) (ext f≡g) p  subst P (f≡g x) p
  subst-ext = subst-good-ext ext′

  elim-ext :
     {a b p} {A : Set a} {B : A  Set b} {x : A}
    (P : B x  B x  Set p)
    (p : (y : B x)  P y y)
    {f g : (x : A)  B x}
    (f≡g :  x  f x  g x) 
    Eq.elim  {f g} _  P (f x) (g x)) (p  (_$ x)) (ext f≡g) 
    Eq.elim  {x y} _  P x y) p (f≡g x)
  elim-ext = elim-good-ext ext′

  -- I based the statements of the following three lemmas on code in
  -- the Lean Homotopy Type Theory Library with Jakob von Raumer and
  -- Floris van Doorn listed as authors. The file was claimed to have
  -- been ported from the Coq HoTT library. (The third lemma has later
  -- been generalised.)

  ext-sym :
     {a b} {A : Set a} {B : A  Set b} {f g : (x : A)  B x}
    (f≡g :  x  f x  g x) 
    ext (sym  f≡g)  sym (ext f≡g)
  ext-sym = good-ext-sym ext′

  ext-trans :
     {a b} {A : Set a} {B : A  Set b} {f g h : (x : A)  B x}
    (f≡g :  x  f x  g x) (g≡h :  x  g x  h x) 
    ext  x  trans (f≡g x) (g≡h x))  trans (ext f≡g) (ext g≡h)
  ext-trans = good-ext-trans ext′

  cong-post-∘-ext :
     {a b c} {A : Set a} {B : A  Set b} {C : A  Set c}
      {f g : (x : A)  B x} {h :  {x}  B x  C x}
    (f≡g :  x  f x  g x) 
    cong (h ∘_) (ext f≡g)  ext (cong h  f≡g)
  cong-post-∘-ext = cong-post-∘-good-ext ext′ ext′

  cong-pre-∘-ext :
     {a b c} {A : Set a} {B : Set b} {C : B  Set c}
      {f g : (x : B)  C x} {h : A  B}
    (f≡g :  x  f x  g x) 
    cong (_∘ h) (ext f≡g)  ext (f≡g  h)
  cong-pre-∘-ext = cong-pre-∘-good-ext ext′ ext′