{-
Auke Booij, February 2016

In Univalent Foundations, if there is a polymorphic function f_X : X → X, such
that f₂ is not the identity function, then LEM holds.

See also the accompanying paper at

http://www.cs.bham.ac.uk/~abb538/papers/2016-02-parametricity.pdf

and the blog post at

http://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/
-}

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

module nonparametric where

open import HoTT

transport-fst :  {i j k} {A : Type i} (B : A  Type j) (C : (z : A)  B z  Type k) {x y : A} (p : x == y) (u : B x) (v : C x u)  fst (transport  z  Σ (B z) (C z)) p (u , v)) == transport B p u
transport-fst B C idp u v = idp
transport-snd' :  {i j k} {A : Type i} (B : A  Type j) (C : A  Type k) {x y : A} (p : x == y) (u : B x) (v : C x)  snd (transport  z  B z × C z) p (u , v)) == transport C p v
transport-snd' B C idp u v = idp

polymorphicFun : Type (lsucc lzero)
polymorphicFun = {X : Type lzero}  X  X

flip : Bool  Bool
flip true = false
flip false = true

flip-eq : Bool  Bool
flip-eq = equiv flip flip flip-id flip-id
  where
  flip-id : (b : Bool)  flip (flip b) == b
  flip-id true = idp
  flip-id false = idp

false-true-fun : Type (lsucc lzero)
false-true-fun = Σ polymorphicFun  f  f {Bool} false  false)

true-false-fun : Type (lsucc lzero)
true-false-fun = Σ polymorphicFun  f  f {Bool} true  true)

is-non-id : {X : Type lzero}  polymorphicFun × X  Type lzero
is-non-id {X} (f , b) = f {X} b  b

non-id-fun : (X : Type lzero)  Type (lsucc lzero)
non-id-fun X = Σ (Σ polymorphicFun  _  X)) is-non-id

prop :  {i}  Type (lsucc i)
prop {i} = Σ (Type i) is-prop

decidable :  {i}  Type i  Type i
decidable X = X  ¬ X

LEM :  {i}  Type (lsucc i)
LEM {i} = (P : prop {i})  decidable (fst P)

efq :  {i} {X : Type i}    X
efq = ⊥-rec

Three :  {i}  (P : prop {i})  Type i
Three P = Suspension (fst P)  Unit

-- re-defining this to get computational equality in the first argument
inhab-prop-is-contr' :  {i} {A : Type i}  A  is-prop A  is-contr A
inhab-prop-is-contr' x₀ p = (x₀ , λ y  fst (p x₀ y))

inhab-susp : {P : prop {lzero}}  fst P  is-contr (Suspension (fst P))
inhab-susp {P} p = north (fst P) , Suspension-elim (fst P) idp (merid (fst P) p) q
  where
  q' : (x : Suspension (fst P)) (q : north (fst P) == x)  PathOver  z  north (fst P) == z) (merid (fst P) p) idp (merid (fst P) p)
  q' x q = J  a' p  PathOver  z  north (fst P) == z) p idp p) idp (merid (fst P) p)
  q : (x : fst P)  PathOver  z  north (fst P) == z) (merid (fst P) x) idp (merid (fst P) p)
  q x =
    transport
       y  PathOver  z  north (fst P) == z) (merid (fst P) y) idp (merid (fst P) p))
      (snd (inhab-prop-is-contr' p (snd P)) x)
      (q' (north (fst P)) idp)

swap :  {i} {X : Type i}  Suspension X  Suspension X
swap = flip-susp

extract : {P : prop {lzero}} (q : north (fst P) == south (fst P))  fst P
extract {P} q = transport code q tt
  where
  code : Suspension (fst P)  Type lzero
  code x = SuspensionRecType.f (fst P) {j = lzero} Unit (fst P)  p  contr-equiv-Unit (inhab-prop-is-contr p (snd P)) ⁻¹) x

↓-contr :  {i j} {A : Type i} {B : A  Type j} {x y : A} {p : x == y} (u : B x) (v : B y)
        (h : (a : A)  is-contr (B a))
         u == v [ B  p ]
↓-contr {_} {_} {_} {_} {x} {_} {idp} u v h = ! (snd (h x) u)  (snd (h x) v)

extract' : {P : prop {lzero}} (x : Suspension (fst P)) (q : x == swap x)  fst P
extract' {P} x q =
  SuspensionElim.f
    (fst P)
    {P = λ x  x == swap x  fst P}
    (extract {P = P})
    ((extract {P = P})  ap swap)
     p  ↓-contr extract (extract  ap swap)  _  WeakFunext.weak-λ=  _  inhab-prop-is-contr p (snd P))))
    x
    q

inhabited-equiv-susp : {P : prop {lzero}}  fst P  Bool  (Three P  Three P)
inhabited-equiv-susp {P} p = equiv f g f-g g-f
  where
  paths : (a b : Suspension (fst P))  inl a == (inl b :> Three P)
  paths a b = ap inl (contr-has-all-paths (inhab-susp {P = P} p) a b)
  three-eq : Three P  Three P
  three-eq = equiv f3 f3 g-f3 g-f3
    where
    f3 : Three P  Three P
    f3 (inr tt) = inl (north (fst P))
    f3 (inl x) = inr tt
    g-f3 : (o : Three P)  f3 (f3 o) == o
    g-f3 (inr tt) = idp
    g-f3 (inl x) = paths (north (fst P)) x
  f : Bool  (Three P  Three P)
  f false = ide (Three P)
  f true = three-eq
  g : (Three P  Three P)  Bool
  g e with –> e (inr tt)
  ... | inr tt = false
  ... | inl _  = true
  g-f : (b : Bool)  g (f b) == b
  g-f false = idp
  g-f true = idp
  deduce-idf : (e : Three P  Three P) (q : –> e (inr tt) == inr tt)  e == ide (Three P)
  deduce-idf e q = subtype=-in is-equiv-is-prop (cases (–> e (inl (north (fst P)))) idp)
    where
    cases : (pt : Three P) (q' : –> e (inl (north (fst P))) == pt)  –> e == idf (Three P)
    cases (inr tt) q' =
      efq (inl≠inr (north (fst P)) tt (
        ! (is-equiv.g-f (snd e) (inl (north (fst P))))
         ap (is-equiv.g (snd e)) (q'  ! q)
         is-equiv.g-f (snd e) (inr tt)
        ))
    cases (inl y)  q' = FunextNonDep.λ=-nondep pted
      where
      pted : (pt' : Three P)  –> e pt' == pt'
      pted (inr tt) = q
      pted (inl z)  = ap (–> e) (paths z (north (fst P)))  q'  paths y z
  deduce-three : (e : Three P  Three P) {u : Suspension (fst P)} (q : –> e (inr tt) == inl u)  e == three-eq
  deduce-three e {u} q = subtype=-in is-equiv-is-prop (cases (–> e (inl u)) idp)
    where
    cases : (pt : Three P) (q' : –> e (inl u) == pt)  –> e == –> three-eq
    cases (inl y)  q' = efq (inl≠inr u tt (
      ! (is-equiv.g-f (snd e) (inl u))
       ap (is-equiv.g (snd e)) (q'  paths y u  ! q)
       is-equiv.g-f (snd e) (inr tt)
      ))
    cases (inr tt) q' = FunextNonDep.λ=-nondep pted
      where
      pted : (pt' : Three P)  –> e pt' == –> three-eq pt'
      pted (inr tt) = q  paths u (north (fst P))
      pted (inl z)  = ap (–> e) (paths z u)  q'  ap (–> three-eq) (paths (north (fst P)) z)
  f-g : (e : Three P  Three P)  f (g e) == e
  f-g e = cases (–> e (inr tt)) idp
    where
    cases : (pt : Three P) (q : –> e (inr tt) == pt)  f (g e) == e
    cases (inr tt) q = transport  d  f (g d) == d) (! (deduce-idf e q)) idp
    cases (inl y) q = transport  d  f (g d) == d) (! (deduce-three e q)) idp

inhabited-equiv-idf : {P : prop {lzero}}  fst P  (e : Three P  Three P)  (–> e (inr tt) == inr tt)  –> e == idf (Three P)
inhabited-equiv-idf {P} p e q = FunextNonDep.λ=-nondep pted
  where
  paths : (a b : Suspension (fst P))  inl a == (inl b :> Three P)
  paths a b = ap inl (contr-has-all-paths (inhab-susp {P = P} p) a b)
  pted : (x : Three P)  –> e x == x
  pted (inl p') = ind (–> e (inl p')) idp
    where
    ind : (y : Three P)  (q' : –> e (inl p') == y)  –> e (inl p') == inl p'
    ind (inl p'') q' = q'  paths p'' p'
    ind (inr tt)  q' =
        q'
       ! (is-equiv.g-f (snd e) (inr tt))
       ap (is-equiv.g (snd e)) (q  ! q')
       is-equiv.g-f (snd e) (inl p')
  pted (inr tt) = q

false-true-LEM : (F : false-true-fun)  LEM {lzero}
false-true-LEM (f , f-neq) P = cases1 (g (inr tt)) idp
  where
  g-eq : Three P  Three P
  g-eq = f {Three P  Three P} (ide (Three P))
  g : Three P  Three P
  g = –> g-eq
  module _ (p : fst P) where
    three-eq : Bool  (Three P  Three P)
    three-eq = inhabited-equiv-susp {P = P} p
    g-neq : Σ (Three P  Three P)  pt  f {Three P  Three P} pt  pt)
    g-neq = transport  X  Σ X  x  f {X} x  x)) (ua three-eq) (false , f-neq)
    g-eq-neq : g-eq  ide (Three P)
    g-eq-neq = transport  x  f x  x) path (snd g-neq)
      where
      path : fst g-neq == ide (Three P)
      path =
          transport-fst
             X  X)
             X x  f {X} x  x)
            (ua three-eq)
            false
            f-neq
         ap
             x  coe x false)
            (ap-idf (ua three-eq))
         coe-β three-eq false
  cases1 : (x : Three P) (q : g (inr tt) == x)  decidable (fst P)
  cases1 (inr tt) q = inr proof
    where
    p1 : (p : fst P)  g == idf (Three P)
    p1 p = inhabited-equiv-idf {P = P} p g-eq q
    proof : (p : fst P)  
    proof p = g-eq-neq p (subtype=-in is-equiv-is-prop (p1 p))
  cases1 (inl x)  q = cases2 (g (inl x)) idp
    where
    cases2 : (y : Three P) (r : g (inl x) == y)  decidable (fst P)
    cases2 (inl y)  r = inr proof
      where
      proof : (p : fst P)  
      proof p = inl≠inr x tt (
        ! (is-equiv.g-f (snd g-eq) (inl x))
         ap (is-equiv.g (snd g-eq)) (r  ap inl (contr-has-all-paths (inhab-susp {P = P} p) y x)  ! q)
         is-equiv.g-f (snd g-eq) (inr tt)
        )
    cases2 (inr tt) r = cases3 (g (inl (swap x))) idp
      where
      cases3 : (z : Three P) (s : g (inl (swap x)) == z)  decidable (fst P)
      cases3 (inl z)  s = inr  p  inr≠inl tt z (
        ! r
         ap (g  inl) (contr-has-all-paths (inhab-susp {P = P} p) x (swap x))
         s)
        )
      cases3 (inr tt) s = inl (extract' {P = P} x (–> (inl=inl-equiv x (swap x)) (
        ! (is-equiv.g-f (snd g-eq) (inl x))
         ap (is-equiv.g (snd g-eq)) (r  ! s)
         is-equiv.g-f (snd g-eq) (inl (swap x))
        )))

true-false-LEM : (F : true-false-fun)  LEM {lzero}
true-false-LEM (f , f-neq) = false-true-LEM (f' , f-neq')
  where
  f-as : non-id-fun Bool
  f-as = ((f , true) , f-neq)
  f-as' : non-id-fun Bool
  f-as' = transport non-id-fun (ua flip-eq) f-as
  f' : polymorphicFun
  f' = fst (fst f-as')
  f-neq' : f' {Bool} false  false
  f-neq' = transport
     b  f' b  b)
    (
      ap snd (
        transport-fst
           X  Σ polymorphicFun  _  X))
           X b  is-non-id {X} b)
          (ua flip-eq)
          (fst f-as)
          f-neq
        )
     transport-snd'  _  polymorphicFun) (idf Set) (ua flip-eq) f true
     ap  x  coe x true) (ap-idf (ua flip-eq))
     coe-β flip-eq true
    )
    (snd f-as')

non-id-LEM : (f : polymorphicFun)  (f {Bool}  idf Bool)  LEM {lzero}
non-id-LEM f neq = cases1 (f false) idp
  where
  cases1 : (b : Bool) (p : f false == b)  LEM {lzero}
  cases1 true  p = false-true-LEM (f , λ q  Bool-false≠true (! q  p))
  cases1 false p = cases2 (f true) idp
    where
    cases2 : (b : Bool) (p : f true == b)  LEM {lzero}
    cases2 true q  = efq (neq (FunextDep.λ= f-id))
      where
      f-id : (b : Bool)  f b == b
      f-id true = q
      f-id false = p
    cases2 false q = true-false-LEM (f ,  r  Bool-true≠false (! r  q)))