weak_univalence.lean

import data.equiv.basic data.option.basic
import tactic
universe u

axiom weak_univalence {α β : Sort*} : α ≃ β → α = β

def propext2 {p q : Prop} (h : p ↔ q) : p = q :=
weak_univalence ⟨h.mp, h.mpr, λ _, rfl, λ _, rfl⟩

section propext_free

lemma option.is_some_of_ne_none {α : Type*} {o : option α} : o ≠ none → o.is_some :=
option.cases_on o (λ h, (h rfl).elim) (λ _ _, rfl)

-- lemma option.some_injective {α : Type*} : function.injective (@some α) :=
-- λ x y h, by injection h

section exact
/- copied from core -/
variables {α : Sort u} [s : setoid α]
include s

private def rel (q₁ q₂ : quotient s) : Prop :=
quotient.lift_on₂ q₁ q₂
  (λ a₁ a₂, a₁ ≈ a₂)
  (λ a₁ a₂ b₁ b₂ a₁b₁ a₂b₂,
    propext2 (iff.intro
      (λ a₁a₂, setoid.trans (setoid.symm a₁b₁) (setoid.trans a₁a₂ a₂b₂))
      (λ b₁b₂, setoid.trans a₁b₁ (setoid.trans b₁b₂ (setoid.symm a₂b₂)))))

local infix `~` := rel

private lemma rel.refl : ∀ q : quotient s, q ~ q :=
λ q, quot.induction_on q (λ a, setoid.refl a)

private lemma eq_imp_rel {q₁ q₂ : quotient s} : q₁ = q₂ → q₁ ~ q₂ :=
assume h, eq.rec_on h (rel.refl q₁)

lemma quotient.exact2 {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b :=
assume h, eq_imp_rel h

end exact

end propext_free

def equiv_of_eq {α β : Sort u} (h : α = β) : α ≃ β :=
{ to_fun := eq.mp h,
  inv_fun := eq.mpr h,
  left_inv := eq.drec_on h (λ _, rfl),
  right_inv := eq.drec_on h (λ _, rfl) }

lemma unique_choice {α : Sort*} (hs : subsingleton α) (h : nonempty α) : α :=
have α = punit, from let ⟨a⟩ := h in weak_univalence
  { to_fun := λ _, punit.star,
    inv_fun := λ _, a,
    left_inv := λ _, subsingleton.elim _ _,
    right_inv := λ _, subsingleton.elim _ _ },
this.mpr punit.star

section option_inj

def option_fun_aux {α β : Type u} (h : option α ≃ option β) (a : α) : option β :=
option.rec_on (h (some a)) (h none) some

def option_fun_aux_is_some {α β : Type u} (e : option α ≃ option β) (a : α) :
  (option_fun_aux e a).is_some :=
begin
  rw [option_fun_aux],
  cases h : e a,
  { dsimp,
    refine option.is_some_of_ne_none _,
    assume h₁,
    rw ← h₁ at h,
    exact option.no_confusion (e.injective h) },
  { exact rfl }
end

def option_fun {α β : Type u} (e : option α ≃ option β) (a : α) : β :=
option.get (option_fun_aux_is_some e a)

def option_fun_option_fun {α β : Type u} (e : option α ≃ option β) (a : α) :
  option_fun e.symm (option_fun e a) = a :=
begin
  rw [option_fun, option_fun],
  apply option.some_injective _,
  rw [option.some_get, option_fun_aux],
  rw option.some_get,
  cases h : e.symm (option_fun_aux e a),
  { rw option_fun_aux at h,
    cases h₂ : e (some a),
    { refine e.injective _,
      dsimp,
      rw [equiv.apply_symm_apply, h₂] },
    { rw h₂ at h,
      dsimp at h,
      rw [← h₂, equiv.symm_apply_apply] at h,
      exact option.no_confusion h } },
  { dsimp,
    rw [option_fun_aux] at h,
    cases h₂ : e (some a),
    { rw h₂ at h,
      dsimp at h,
      rw [equiv.symm_apply_apply] at h,
      exact option.no_confusion h },
    { rw h₂ at h,
      dsimp at h,
      have := congr_arg e h,
      rw equiv.apply_symm_apply at this,
      rw this at h₂,
      exact (e.injective h₂).symm } }
end

lemma option_inj_aux {α β : Type u} (e : option α ≃ option β) : α = β :=
weak_univalence
  { to_fun := option_fun e,
    inv_fun := option_fun e.symm,
    left_inv := option_fun_option_fun _,
    right_inv := λ _, begin
      conv in e {rw ← e.symm_symm },
      rw [option_fun_option_fun]
    end }

lemma option_inj {α β : Type u} (e : option α = option β) : α = β :=
option_inj_aux (equiv_of_eq e)

end option_inj

lemma nonempty_equiv_option {α : Type*} [decidable_eq α] : nonempty α →
  nonempty {β : Type u // option β = α} :=
λ ⟨a⟩, ⟨⟨{b : α // b ≠ a}, weak_univalence
{ to_fun := λ b, option.cases_on b a subtype.val,
  inv_fun := λ b, if hba : b = a then none else some ⟨b, hba⟩,
  left_inv := λ b, option.cases_on b (dif_pos rfl) (λ ⟨_, _⟩, dif_neg _),
  right_inv := λ b, if h : b = a then by dsimp; rw [h, dif_pos rfl]
    else by dsimp; rw dif_neg h }⟩⟩

lemma decidable_choice {α : Sort u} [decidable_eq α] : nonempty α → α :=
λ h, have {β : Type u // option β = plift α},
  from unique_choice ⟨λ x y, subtype.eq $ option_inj $ by rw [x.2, y.2]⟩
    (nonempty.elim h (λ a, nonempty_equiv_option ⟨plift.up a⟩)),
plift.rec_on (this.2.mp none) id

section em
parameter (p : Prop)

def r : setoid bool :=
  { r := λ x y : bool, p ∨ x = y,
    iseqv := ⟨λ _, or.inr rfl,
      λ x y hxy, hxy.elim or.inl (or.inr ∘ eq.symm),
      λ x y z hxy hyz, hxy.elim or.inl
        (λ hxy, hyz.elim or.inl (λ hyz, or.inr $ by rw [hxy, hyz]))⟩ }

def suspension : Type := quotient r

instance suspension_to_bool_decidable : decidable_eq (suspension → bool) :=
λ f g, decidable_of_iff (f (quot.mk _ tt) = g (quot.mk _ tt) ∧
  (f (quot.mk _ ff) = g (quot.mk _ ff)))
  ⟨λ hfg, funext $ λ s, quot.ind (λ b, bool.cases_on b hfg.2 hfg.1) s,
    λ hfg, by rw hfg; exact ⟨rfl, rfl⟩⟩

lemma nonempty_subtype_bool (s : suspension) : nonempty
  {b : bool // @quotient.mk _ r b = s} :=
let ⟨b, hb⟩ := quot.exists_rep s in ⟨⟨b, hb⟩⟩

lemma g (s : suspension) : bool :=
(decidable_choice (nonempty_subtype_bool s)).1

set_option type_context.unfold_lemmas true
lemma quot_mk_g (s : suspension) : quotient.mk' (g s) = s :=
(decidable_choice (nonempty_subtype_bool s)).2

lemma g_injective : function.injective g :=
function.left_inverse.injective quot_mk_g

lemma p_iff_g_tt_eq_g_ff : p ↔ g (quotient.mk' tt) = g (quotient.mk' ff) :=
⟨λ hp, congr_arg _ (quotient.sound' (or.inl hp)),
  λ h, (@quotient.exact2 _ (id _) _ _ (g_injective h)).elim
    id
    (λ h, bool.no_confusion h)⟩

lemma prop_decidable : decidable p :=
decidable_of_iff _ p_iff_g_tt_eq_g_ff.symm

end em

def choice {α : Sort u} : nonempty α → α :=
@decidable_choice α (λ _ _, prop_decidable _)

#print axioms choice