------------------------------------------------------------------------
-- 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)
import Equality.Propositional.Rewriting
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

-- The definition of bad-ext has been placed in a separate abstract
-- block to ensure that the definitions in the other abstract block
-- below do not accidentally depend on the implementation of bad-ext.

private
 module Separate-abstract-block where

  abstract

    -- The interval can be used to prove that equality of functions is
    -- extensional.
    --
    -- The proof bad-ext is perhaps not less "good" than ext (I don't
    -- know), it is called this simply because it is not defined using
    -- good-ext.

    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

    bad-ext :  {a b}  Extensionality a b
    apply-ext bad-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]  

open Separate-abstract-block public

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

⟨ext⟩ :  {a b} {A : Set a} {B : A  Set b}  Extensionality′ A B
⟨ext⟩ = apply-ext ext

abstract

  -- 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 bad-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 bad-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 bad-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 bad-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 bad-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 bad-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 bad-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 bad-ext bad-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 bad-ext bad-ext