\import Algebra.Monoid
\import Algebra.Monoid.Sub
\import Algebra.Ring
\import Algebra.Ring.Localization
\import Algebra.Ring.RingCategory
\import Algebra.Ring.RingHom
\import Category
\import Function.Meta
\import Logic
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set

\sfunc localization-unique {R : CRing} {S : SubSet R} (l1 l2 : Localization R S) : l1 = l2
  => \have e => lift-iso S S l1 l2 l1.local l2.local
     \in ext (Cat.isotoid e, Cat.transport_Hom_iso-right e l1.inL (l1.lift-prop l2.inL l2.local))
  \where {
    \lemma lift-iso {R : CRing} (S1 S2 : SubSet R) (l1 : Localization R S1) (l2 : Localization R S2)
                    (p1 : \Pi (x : R) -> S2 x -> Monoid.Inv (l1.inL x)) (p2 : \Pi (x : R) -> S1 x -> Monoid.Inv (l2.inL x))
      : Iso (l1.lift l2.inL p2) \cowith
      | hinv => l2.lift l1.inL p1
      | hinv_f => l1.remove_inL {l1.R'} (l2.lift l1.inL p1 ∘ l1.lift l2.inL p2) (id l1.R')
                  \lam x => pmap (l2.lift l1.inL p1) (l1.lift-prop-func l2.inL p2 x) *> l2.lift-prop-func l1.inL p1 x
      | f_hinv => l2.remove_inL {l2.R'} (l1.lift l2.inL p2 ∘ l2.lift l1.inL p1) (id l2.R')
                  \lam x => pmap (l1.lift l2.inL p2) (l2.lift-prop-func l1.inL p1 x) *> l1.lift-prop-func l2.inL p2 x
  }

\lemma localization-closure-equiv {R : CRing} (S : SubSet R) (l1 : Localization R S) (l2 : Localization R (closure S))
  : Iso (l1.lift l2.inL (\lam x x<-S => l2.local x (closure.ext S x x<-S)))
  => localization-unique.lift-iso S (closure S) l1 l2 (inv-closure l1) (\lam x x<-S => l2.local x (closure.ext S x x<-S))
  \where {
    \open SubMonoid

    \lemma inv-closure (l : Localization R S) (x : R) (p : closure S x) : Monoid.Inv (l.inL x) \elim p
      | inP (, p) => l.local x p
      | inP (suc n, byLeft x<-C) => inv-closure l x (inP (n, x<-C))
      | inP (suc n, byRight (byLeft x=1)) => rewrite (pmap l.inL x=1 *> l.inL.func-ide) Monoid.Inv.ide-isInv
      | inP (suc n, byRight (byRight (y, z, y<-C, z<-C, x=y*z))) => rewrite (pmap l.inL x=y*z *> l.inL.func-*) (Monoid.Inv.product (inv-closure l y (inP (n, y<-C))) (inv-closure l z (inP (n, z<-C))))
  }

\lemma locMap-epi {R : CRing} {S : SubMonoid R} : isEpi (locMap {R} {S})
  => \lam q => RingHom.equals $ localization.locMap-epiMap _ _ \lam a i => q i a