\import Algebra.Group
\import Algebra.Monoid
\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 (rewriteEq (pmap (negative x +) 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 (_ +) negative_*-right *> toZero (ide-right *> inv p)
                   \in \case loc (negative a) \with {
                     | byLeft (r : Inv) => byRight $ inv $ fromZero $ +-comm *> inv ide-left *> pmap (`* _) (inv r.inv-left) *> *-assoc *> pmap (r.inv *) (negative_*-left *> pmap negative q *> 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