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

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

\class Choice \extends BaseSet {
| choice {B : E -> \Set} : (\Pi (x : E) -> TruncP (B x)) -> TruncP (\Pi (x : E) -> B x)

\lemma liftDepSurj {A : E -> \Set} {B : E -> \1-Type} {f : \Pi {x : E} -> A x -> B x} (isSur : \Pi {x : E} (y : B x) -> TruncP (Fib f y)) (g : \Pi (x : E) -> B x) : ∃ (g' : \Pi (x : E) -> A x) ∀ x (f (g' x) = g x)
=> TruncP.map (choice (\lam x => isSur (g x))) (\lam h => (\lam x => (h x).1, \lam x => (h x).2))

\lemma liftSurj {A : \Set} {B : \1-Type} {f : A -> B} (isSur : \Pi (y : B) -> TruncP (Fib f y)) (g : E -> B) : ∃ (g' : E -> A) ∀ x (f (g' x) = g x)
=> liftDepSurj (\lam {_} => isSur) g
}

\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, flase => 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)).1 \as x, idp : (f (in~ true)).1 = x, (f (in~ false)).1 \as y, idp : (f (in~ false)).1 = y \with {
| true, p, true, q => yes (Quotient.equalityEquiv E (pmap in~ (inv q) *> (f (in~ false)).2))
| true, p, false, q => no (\lam a => true/=false (inv p *> path (\lam i => (f (~-equiv true false a i)).1) *> q))
| false, p, true, q => no (\lam a => true/=false (inv q *> path (\lam i => (f (~-equiv false true a i)).1) *> p))
| false, p, false, q => yes (Quotient.equalityEquiv E (inv (f (in~ true)).2 *> pmap in~ p))
}
}
}