\import Data.Bool
\import Homotopy.Fibration
\import Logic
\import Logic.Meta
\import Paths
\import Relation.Equivalence
\import Set

\axiom alem (P : \Prop) : Dec P

\axiom achoice {A : \Set} (B : A -> \Set) : (\Pi (x : A) -> TruncP (B x)) -> TruncP (\Pi (x : A) -> B x)
  \where {
    \lemma lemFromChoice (P : \Prop) : Dec P
      => \let | R (x y : Bool) : \Prop => \case x, y \with {
                                       | true, true => \Sigma
                                       | true, false => P
                                       | false, true => P
                                       | false, false => \Sigma
                                     }
              | E => \new Equivalence Bool {
                | ~ => R
                | ~-reflexive {b} => \case \elim b \with {
                  | true => ()
                  | false => ()
                }
                | ~-symmetric {a} {b} p => \case \elim a, \elim b, p \with {
                  | true, true, _ => ()
                  | true, false, p => p
                  | false, true, p => p
                  | false, false, _ => ()
                }
                | ~-transitive {a} {b} {c} p q => \case \elim a, \elim b, \elim c, p, q \with {
                  | true, _, true, _, _ => ()
                  | false, _, false, _, _ => ()
                  | true, true, false, p, q => q
                  | true, false, false, p, q => p
                  | false, true, true, p, q => p
                  | false, false, true, p, q => q
                }
              }
         \in \case achoice (\lam q => \Sigma (x : Bool) (in~ x = q)) (\lam (in~ x) => inP (x,idp)) \with {
               | inP f =>
                 \case (f (in~ true)). \as x, idp : (f (in~ true)). = x, (f (in~ false)). \as y, idp : (f (in~ false)). = y \with {
                   | true, p, true, q => yes (Quotient.equalityEquiv E (pmap in~ (inv q) *> (f (in~ false)).))
                   | true, p, false, q => no (\lam a => true/=false (inv p *> path (\lam i => (f (~-equiv true false a i)).) *> q))
                   | false, p, true, q => no (\lam a => true/=false (inv q *> path (\lam i => (f (~-equiv false true a i)).) *> p))
                   | false, p, false, q => yes (Quotient.equalityEquiv E (inv (f (in~ true)). *> pmap in~ p))
                 }
             }
  }