\import Homotopy.Space
\import Logic
\import Meta
\import Paths
\import Paths.Meta

\class Pointed \extends InhSpace
  | base : E
  | isInh => inP base
  \where
    \func make {E : \Type} (e : E) => \new Pointed E e

\instance UnitPointed : Pointed (\Sigma)
  | base => ()

\func \infixr  ->* (A B : Pointed) => \Sigma (f : A -> B) (f base = base)
  \where {
    \func ext {A B : Pointed} {f g : A ->* B} (p : \Pi (x : A) -> f. x = g. x) (q : p base *> g. = f.) : f = g =>
      \let | p' => path (\lam i x => p x @ i)
           | q' => Jl (\lam _ p'' => (rewrite p'' in f.) = inv (pmap (\lam (h : A -> B) => h base) p'') *> f.)
                      (inv (idp_*> _)) p' *> rotatePathLeft (inv q)
      \in path (\lam i => (p' @ i, pathOver q' @ i))
  }