Lagrange

\import Algebra.Group
\import Algebra.Group.Sub
\import Algebra.Monoid
\import Equiv
\import Equiv.Univalence
\import Function.Meta
\import Logic
\import Logic.Classical
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\open Group

\lemma lagrange-gen (H : SubGroup) (c : Choice H.Cosets) : TruncP (H.S = {\Set} (\Sigma H.Cosets H.struct))
  => TruncP.map (c.choice {\lam x => \Sigma (y : H.S) (x = in~ y)} (\case \elim __ \with { | in~ y => inP (y,idp) })) $ \lam e => QEquiv-to-= $
      \new QEquiv {
        | f x => (in~ x, \let t => e (in~ x) \in (inverse x * t.1, Quotient.equalityEquiv SubGroup.equivalence t.2))
        | ret s => (e s.1).1 * inverse s.2.1
        | ret_f x => rewrite (inverse_*, inverse-isInv, inv *-assoc, inverse-right) ide-left
        | f_sec s => \have p : in~ ((e s.1).1 * inverse s.2.1) = s.1 => ~-pequiv (later $ rewrite (inverse_*, inverse-isInv, *-assoc, inverse-left, ide-right) s.2.2) *> inv (e s.1).2
                     \in unfold_let $ pmap2 (__,__) p $ ext $ rewrite (p, inverse_*, inverse-isInv, *-assoc, inverse-left) ide-right
      }