\import Equiv
\import Equiv.Path
\import Paths

\func Total {B : \Type} (F : B -> \Type) => \Sigma (b : B) (F b)
\where
\func proj (F : B -> \Type) => \lam (t : Total F) => t.1

\func Fib {A B : \Type} (f : A -> B) (base : B) => \Sigma (a : A) (f a = base)
\where {
\func make {base : B} (a : A) (p : f a = base) : Fib f base => (a,p)

\func ext (b0 : B) (x x' : Fib f b0) (p : x.1 = x'.1) (q : pmap f p *> x'.2 = x.2) : x = x'
=> (retraction b0 x' x p q).1
\where
\func retraction (b0 : B) (x' x : Fib f b0) (p : x.1 = x'.1) (q : pmap f p *> x'.2 = x.2)
: \Sigma (t : x = x') (transport (\lam x'' => \Sigma (p : x.1 = x''.1) (pmap f p *> x''.2 = x.2)) t (idp, idp_*> x.2) = (p,q)) \elim x', x, p, q
| (x'1,idp), (x1,x2), idp, idp => (idp,idp)

\func equiv (b0 : B) (x x' : Fib f b0) : QEquiv {x = x'} {\Sigma (p : x.1 = x'.1) (pmap f p *> x'.2 = x.2)} =>
\let S {b0 : B} (x x' : Fib f b0) => \Sigma (p : x.1 = x'.1) (pmap f p *> x'.2 = x.2)
\in pathEquiv S (\lam {x x' : Fib f b0} =>
\new Retraction {
| f q => transport (S x) q (idp, idp_*> x.2)
| sec s => ext b0 x x' s.1 s.2
| f_sec s => (ext.retraction b0 x' x s.1 s.2).2
})
}