choice_univalence

universe u

inductive EQ {α : Type u} (a : α) : α → Type
| refl : EQ a

def casT {α β : Type} (h : EQ α β) (a : α) : β :=
@EQ.rec_on Type α (λ A hA, A) β h a

def EQ.trans {α : Type u} {a b c : α} (h₁ : EQ a b) (h₂ : EQ b c) : EQ a c :=
@EQ.rec_on α b (λ A hA, EQ a A) c h₂ h₁

def congr_arg_EQ {α β : Type u} {f : α → β} {a b : α} (h : EQ a b) : 
  EQ (f a) (f b) :=
@EQ.rec_on α a (λ c hc, EQ (f a) (f c)) b h EQ.refl

constant squash (α : Type) : Type

constant squash_EQ {α : Type} (a b : squash α) : EQ a b

constant to_squash {α : Type} (a : α) : squash α

constant choice : ∀ (α : Type), squash α → α

noncomputable example (swap : EQ bool bool) : 
  EQ (choice bool (to_squash ff) : bool) 
  (casT swap (choice bool (to_squash ff))) :=
have h : _ := @EQ.rec_on Type bool 
  (λ A hA, EQ (choice A (to_squash (casT hA ff))) (casT hA (choice bool (to_squash ff)))) 
    bool swap EQ.refl,
EQ.trans (congr_arg_EQ (squash_EQ _ _)) h