\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Semiring
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\open Monoid(Inv,LInv)

\class LocalRing \extends Ring, NonZeroRing {
  | locality (x : E) : Inv x || Inv (x + ide)

  \lemma locality_- (x : E) : Inv x || Inv (ide - x)
    => \case locality (negative x) \with {
      | byLeft p => byLeft $ transport Inv negative-isInv (Ring.negative_inv p)
      | byRight p => byRight $ transport Inv +-comm p
    }

  \lemma sum1=>eitherInv {x y : E} (x+y=1 : x + y = ide) : Inv x || Inv y => \case locality (negative x) \with {
    | byLeft -x_inv => byLeft (rewriteI negative-isInv (Ring.negative_inv -x_inv))
    | byRight [-x+1]_inv => byRight $ transport Inv (equation.abGroup { -1 x+y=1 }) [-x+1]_inv
  }

  \lemma sumInv=>eitherInv {x y : E} (q : Inv (x + y)) : Inv x || Inv y =>
    \case sum1=>eitherInv (inv ldistr *> q.inv-left) \with {
      | byLeft s => byLeft (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
      | byRight s => byRight (Inv.factor-right (\new LInv q.inv (x + y) q.inv-right) s)
    }

  \lemma sumInvArray (l : Array E) (p : Inv (BigSum l)) : ∃ (j : Fin l.len) (Inv (l j)) \elim l
    | nil => absurd (NonZeroSemiring.inv-nonZero p idp)
    | a :: l => \case sumInv=>eitherInv p \with {
      | byLeft r => inP (, r)
      | byRight r => TruncP.map (sumInvArray l r) \lam s => (suc s., s.)
    }

  \lemma sum1Array (l : Array E) (p : BigSum l = ) : ∃ (j : Fin l.len) (Inv (l j))
    => sumInvArray l (transportInv Inv p Inv.ide-isInv)

  \lemma connected : IsConnected
    => local=>connected locality
} \where {
  \lemma local=>connected {R : Ring} (loc : \Pi (a : R) -> Inv a || Inv (a + )) : R.IsConnected
    => \lam a p => \have q : a * (negative a + ) =  => ldistr *> +-comm *> pmap (_ +) R.negative_*-right *> R.toZero (ide-right *> inv p)
                   \in \case loc (negative a) \with {
                     | byLeft (r : Inv) => byRight $ inv $ R.fromZero $ +-comm *> inv ide-left *> pmap (`* _) (inv r.inv-left) *> *-assoc *> pmap (r.inv *) (R.negative_*-left *> pmap negative q *> R.negative_zro) *> zro_*-right
                     | byRight (r : Inv) => byLeft $ inv ide-right *> pmap (a *) (inv r.inv-right) *> inv *-assoc *> pmap (`* r.inv) q *> zro_*-left
                   }
}

\class LocalCRing \extends LocalRing, NonZeroCRing