\import Homotopy.Pushout
\import Homotopy.Space
\import Homotopy.Suspension
\import Logic
\import Paths

\class Connected0 \extends InhSpace
  | isConn0 (x y : E) : TruncP (x = y)

\instance UnitConnected0 : Connected0 (\Sigma)
  | isInh => inP ()
  | isConn0 _ _ => inP idp

\instance PushoutConnected0 {A : InhSpace} {B C : Connected0} {f : A -> B} {g : A -> C} : Connected0 (PushoutData f g)
  | isInh => \case isInh \with {
    | inP b => inP (pinl b)
  }
  | isConn0 x y => \case isInh, \elim x, \elim y \with {
    | inP a, pinl b, pinl b' => TruncP.map (isConn0 b b') (pmap pinl)
    | inP a, pinl b, pinr c => \case isConn0 b (f a), isConn0 (g a) c \with {
      | inP p, inP q => inP (pmap pinl p *> path (pglue a) *> pmap pinr q)
    }
    | inP a, pinr c, pinl b => \case isConn0 c (g a), isConn0 (f a) b \with {
      | inP p, inP q => inP (pmap pinr p *> inv (path (pglue a)) *> pmap pinl q)
    }
    | inP a, pinr c, pinr c' => TruncP.map (isConn0 c c') (pmap pinr)
  }