Algebra.groupIso

-- KERNEL, IMAGE, AND THE FIRST ISOMORPHISM THEOREM.
--
-- The kernel is an Ω-valued predicate — it has to be, to be quotiented
-- by — and it is an EQUATION, which is the cheapest kind of Ω-valued
-- predicate there is: every membership proof is ⋆ and every membership
-- fact is reflected into a judgemental equality on the spot.

import Core.id (Id, idToEq, eqToId, refl)
import Core.prelude (funext)
import Core.bracket (Br, br, brElim, brIsProp)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Algebra.groupTheory (gop, ge, ginv, gAssoc, gUnitL, gUnitR, gInvL, gInvR, gCancelInner, gCancelInnerInv, gCancelOuter, gCancelOuterInv, gInvUniq, gInvInv, gInvUnit, gOpInv, gCancelL, gCancelR, gEqOfOpInvUnit)
import Algebra.subgroup (IsSubgroup, IsNormal, sgIntro, sgUnit, sgOp, sgInv, nmIntro, nmConj, nmConjInv, cosetRel, cosetRefl, cosetSymm, cosetTrans)
import Algebra.quotGroup (QGroup, qcls, qclsEq, qclsEffective, qMul, qMulCls, qInv, qInvCls, qUnit, qIsGroup, qFactor, qFactorCls, qFactorUnique)
import Algebra.groupHom (IsHom, Hom, homAp, homIntro, homLaw, homIntroAp, homUnit, homInv, homOpInv, qopIsQMul, qeIsQUnit, qinvIsQInv, qProj, qProjAp, homKillConst, homQuotMap, homQuotMapCls, homQuot, homQuotFactors, homQuotUnique)
import Core.equality (transportP, transport, sym, trans, cong, pairext)

ker : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) → G → Ω
ker = λG g H h p x. homAp p x ≡ ge h

kerOp : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (x y : G)
  → ker _ _ _ _ p x → ker _ _ _ _ p y → ker _ _ _ _ p (gop g x y)
  using (ker.eq)
kerOp =
  λG g H h p x y hx hy. homAp p (gop g x y)
    ≡⟨ homLaw p x y ⟩ gop h (homAp p x) (homAp p y)
    ≡⟨ cong (λw. H) (λw. gop h w (homAp p y)) hx ⟩ gop h (ge h) (homAp p y)
    ≡⟨ cong (λw. H) (λw. gop h (ge h) w) hy ⟩ gop h (ge h) (ge h)
    ≡⟨ gUnitL h (ge h) ⟩ ge h

kerInv : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (x : G)
  → ker _ _ _ _ p x → ker _ _ _ _ p (ginv g x)
  using (ker.eq)
kerInv =
  λG g H h p x hx. homAp p (ginv g x)
    ≡⟨ homInv p x ⟩ ginv h (homAp p x)
    ≡⟨ cong (λw. H) (λw. ginv h w) hx ⟩ ginv h (ge h)
    ≡⟨ gInvUnit h ⟩ ge h

kerIsSubgroup : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  → IsSubgroup g (ker _ _ _ _ p)
  using (ker.eq)
kerIsSubgroup = λG g H h p. sgIntro (homUnit p) (kerOp _ _ _ _ p) (kerInv _ _ _ _ p)

-- normality, with no case analysis at all: f (x·n·x⁻¹) = f x · e · f x⁻¹
-- and the two outer factors annihilate
kerIsNormal : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  → IsNormal g (ker _ _ _ _ p)
  using (ker.eq)
kerIsNormal =
  λG g H h p. nmIntro
    λx n hn. homAp p (gop g x (gop g n (ginv g x)))
      ≡⟨ homLaw p x (gop g n (ginv g x)) ⟩ gop h (homAp p x) (homAp p (gop g n (ginv g x)))
      ≡⟨ cong (λw. H) (λw. gop h (homAp p x) w) (homLaw p n (ginv g x)) ⟩
        gop h (homAp p x) (gop h (homAp p n) (homAp p (ginv g x)))
      ≡⟨ cong (λw. H) (λw. gop h (homAp p x) (gop h w (homAp p (ginv g x)))) hn ⟩
        gop h (homAp p x) (gop h (ge h) (homAp p (ginv g x)))
      ≡⟨ cong (λw. H) (λw. gop h (homAp p x) w) (gUnitL h (homAp p (ginv g x))) ⟩
        gop h (homAp p x) (homAp p (ginv g x))
      ≡⟨ cong (λw. H) (λw. gop h (homAp p x) w) (homInv p x) ⟩
        gop h (homAp p x) (ginv h (homAp p x))
      ≡⟨ gInvR h (homAp p x) ⟩ ge h

-- ===== the image, with the BRACKET =====
--
-- This is the choice the whole theorem turns on. The obvious spelling
--
--   im p ≜ ((y : H) × ∥(x : G) × Id H (p x) y∥)
--
-- is unusable: ∥·∥ lives in Ω, el-squash-e-prf reaches only further
-- PROPOSITIONS, and the inverse map G/ker p ← im p has to land in
-- DATA. With that definition the first isomorphism theorem is simply
-- not provable, and that is not a defect — it is the constructive
-- content of the statement.
--
-- Core/bracket.nova's Br is the other truncation: Br a ≜ a / (x y.
-- ∥𝟙∥), a 𝕌-CODE whose `class` RETAINS its representative, so brElim
-- lands in an arbitrary type at the price of a constancy proof.
-- Defining
--
--   Im p ≜ ((y : H) × Br ((x : G) × Id H (p x) y))
--
-- makes the inverse map writable, and the constancy obligation brElim
-- charges for it is EXACTLY "any two preimages of y agree modulo
-- ker p" — the mathematical content of the theorem, paid at the point
-- where it is used rather than assumed at the point where the image is
-- defined. See fromImAt below; that one obligation is the proof.
--
-- Br is also a DEFINITIONAL subsingleton (brIsProp concludes ≐), so
-- two elements of Im with equal first components are equal outright,
-- and every law of Im reduces to the corresponding law of H.
imFib : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) (y : H) → 𝕌
imFib = λG g H h p y. (x : G) × Id _ (homAp p x) y

Im : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) → 𝕌
Im = λG g H h p. (y : H) × Br (imFib _ _ _ _ p y)

-- an element of the image is determined by its H-component
imEq : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u v : Im _ _ _ _ p)
  → (u .π₁ ≡ v .π₁) → u ≡ v
  using (Im.unfold)
imEq = λG g H h p u v e. pairext e (brIsProp (u .π₂) (v .π₂))

imIn : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) (x : G) → Im _ _ _ _ p
  using (Im.unfold, imFib.unfold, Core.id.Id.eq)
imIn = λG g H h p x. homAp p x, br (x, refl H (homAp p x))

-- ===== the fibres are closed under the group operations =====
imFibOp : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {y1 y2 : H}
  (f1 : imFib _ _ _ _ p y1)
  (f2 : imFib _ _ _ _ p y2)
  → imFib _ _ _ _ p (gop h y1 y2)
  using (imFib.unfold)
imFibOp =
  λG g H h p y1 y2 f1 f2. (,)
    gop g (f1 .π₁) (f2 .π₁)
    eqToId
      _
      _
      homAp p (gop g (f1 .π₁) (f2 .π₁))
        ≡⟨ homLaw p (f1 .π₁) (f2 .π₁) ⟩ gop h (homAp p (f1 .π₁)) (homAp p (f2 .π₁))
        ≡⟨ cong (λw. H) (λw. gop h w (homAp p (f2 .π₁))) (idToEq _ _ _ (f1 .π₂)) ⟩
          gop h y1 (homAp p (f2 .π₁))
        ≡⟨ cong (λw. H) (λw. gop h y1 w) (idToEq _ _ _ (f2 .π₂)) ⟩ gop h y1 y2

imFibInv : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {y : H}
  (f : imFib _ _ _ _ p y)
  → imFib _ _ _ _ p (ginv h y)
  using (imFib.unfold)
imFibInv =
  λG g H h p y f. (,)
    ginv g (f .π₁)
    eqToId
      _
      _
      homAp p (ginv g (f .π₁))
        ≡⟨ homInv p (f .π₁) ⟩ ginv h (homAp p (f .π₁))
        ≡⟨ cong (λw. H) (λw. ginv h w) (idToEq _ _ _ (f .π₂)) ⟩ ginv h y

-- ...and the same, one bracket up. Every constancy proof here is
-- brIsProp: the target is itself a bracket, so nothing is owed
imOpBrAt : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {y1 y2 : H}
  (f1 : imFib _ _ _ _ p y1)
  (w2 : Br (imFib _ _ _ _ p y2))
  → Br (imFib _ _ _ _ p (gop h y1 y2))
imOpBrAt =
  λG g H h p y1 y2 f1 w2. brElim
    λf2. br (imFibOp f1 f2)
    λf2 f2'. brIsProp (br (imFibOp f1 f2)) (br (imFibOp f1 f2'))
    w2

imOpBr : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {y1 y2 : H}
  (w1 : Br (imFib _ _ _ _ p y1))
  (w2 : Br (imFib _ _ _ _ p y2))
  → Br (imFib _ _ _ _ p (gop h y1 y2))
imOpBr =
  λG g H h p y1 y2 w1 w2. brElim
    λf1. imOpBrAt f1 w2
    λf1 f1'. brIsProp (imOpBrAt f1 w2) (imOpBrAt f1' w2)
    w1

imInvBr : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {y : H}
  (w : Br (imFib _ _ _ _ p y))
  → Br (imFib _ _ _ _ p (ginv h y))
imInvBr =
  λG g H h p y w. brElim
    λf. br (imFibInv f)
    λf f'. brIsProp (br (imFibInv f)) (br (imFibInv f'))
    w

-- ===== the image is a group =====
imOp : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  → Im _ _ _ _ p → Im _ _ _ _ p → Im _ _ _ _ p
  using (Im.unfold)
imOp = λG g H h p u v. gop h (u .π₁) (v .π₁), imOpBr (u .π₂) (v .π₂)

imUnit : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) → Im _ _ _ _ p
  using (Im.unfold, imFib.unfold)
imUnit = λG g H h p. ge h, br (ge g, eqToId _ _ (homUnit p))

imInv : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) → Im _ _ _ _ p → Im _ _ _ _ p
  using (Im.unfold)
imInv = λG g H h p u. ginv h (u .π₁), imInvBr (u .π₂)

imIsGroup : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) → IsGroup (Im _ _ _ _ p)
  using (Algebra.group.IsGroup.unfold,
    Algebra.monoid.IsMonoid.unfold,
    Im.unfold,
    imOp.eq,
    imUnit.eq,
    imInv.eq)
imIsGroup =
  λG g H h p. (,)
    (,)
      imOp _ _ _ _ _
      imUnit _ _ _ _ _
      λx y z. eqToId
        _
        _
        imEq
          _
          _
          _
          _
          _
          imOp _ _ _ _ _ (imOp _ _ _ _ _ x y) z
          imOp _ _ _ _ _ x (imOp _ _ _ _ _ y z)
          gAssoc h (x .π₁) (y .π₁) (z .π₁)
      λx. eqToId _ _ (imEq _ _ _ _ _ (imOp _ _ _ _ _ (imUnit _ _ _ _ p) x) _ (gUnitL h (x .π₁)))
      λx. eqToId _ _ (imEq _ _ _ _ _ (imOp _ _ _ _ _ x (imUnit _ _ _ _ p)) _ (gUnitR h (x .π₁)))
    imInv _ _ _ _ _
    λx. eqToId
      _
      _
      imEq _ _ _ _ _ (imOp _ _ _ _ _ (imInv _ _ _ _ _ x) x) (imUnit _ _ _ _ p) (gInvL h (x .π₁))
    λx. eqToId
      _
      _
      imEq _ _ _ _ _ (imOp _ _ _ _ _ x (imInv _ _ _ _ _ x)) (imUnit _ _ _ _ p) (gInvR h (x .π₁))

-- ===== G/ker p  →  im p =====
--
-- The forward map is a descent out of the quotient, and its constancy
-- proof is Algebra.groupHom.homKillConst at N ≜ ker p — where "kills N"
-- is the identity function, because membership in the kernel IS the
-- equation it has to produce.
kerKills : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (x : G)
  → ker _ _ _ _ p x → homAp p x ≡ ge h
  using (ker.eq)
kerKills = λG g H h p x k. k

toImConst : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (a a' : G)
  → cosetRel g (ker _ _ _ _ p) a a' → imIn _ _ _ _ p a ≡ imIn _ _ _ _ _ a'
  using (imIn.eq)
toImConst = λG g H h p a a' r. imEq _ _ _ _ _ _ _ (homKillConst _ p (kerKills _ _ _ _ p) _ _ r)

toImMap : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  → QGroup _ g (ker _ _ _ _ p) → Im _ _ _ _ p
toImMap = λG g H h p u. qFactor _ _ _ (imIn _ _ _ _ p) (toImConst _ _ _ _ p) u

toImCls : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (a : G)
  → toImMap _ _ _ _ p (class a) ≡ imIn _ _ _ _ _ a
  using (Algebra.quotGroup.QGroup.unfold, toImMap.eq)
toImCls = λG g H h p a. qFactorCls _ _ _ _ (imIn _ _ _ _ p) (toImConst _ _ _ _ p) a

imInOp : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (a b : G)
  → imIn _ _ _ _ p (gop g a b) ≡ imOp _ _ _ _ _ (imIn _ _ _ _ p a) (imIn _ _ _ _ p b)
  using (imIn.eq, imOp.eq)
imInOp = λG g H h p a b. imEq _ _ _ _ _ _ _ (homLaw p a b)

toImLawQ : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {u v : QGroup _ g (ker _ _ _ _ p)}
  → toImMap _ _ _ _ _ (qMul _ _ _ (kerIsNormal _ _ _ _ p) u v)
    ≡ imOp _ _ _ _ _ (toImMap _ _ _ _ _ u) (toImMap _ _ _ _ _ v)
  using (Algebra.quotGroup.QGroup.unfold)
toImLawQ =
  λG g H h p u v. quot-elim
    a. quot-elim
      b. toImMap _ _ _ _ _ (qMul _ _ _ (kerIsNormal _ _ _ _ p) (class a) (class b))
        ≡⟨ cong
          λw. Im _ _ _ _ p
          λw. toImMap _ _ _ _ _ w
          qMulCls _ _ _ (kerIsNormal _ _ _ _ p) a b ⟩
          toImMap _ _ _ _ _ (class (gop g a b))
        ≡⟨ toImCls _ _ _ _ p (gop g a b) ⟩ imIn _ _ _ _ _ (gop g a b)
        ≡⟨ imInOp _ _ _ _ p a b ⟩ imOp _ _ _ _ _ (imIn _ _ _ _ p a) (imIn _ _ _ _ p b)
        ≡⟨ cong
          λw. Im _ _ _ _ p
          λw. imOp _ _ _ _ _ w (imIn _ _ _ _ p b)
          sym _ _ (toImCls _ _ _ _ p a) ⟩
          imOp _ _ _ _ _ (toImMap _ _ _ _ p (class a)) (imIn _ _ _ _ p b)
        ≡⟨ cong
          λw. Im _ _ _ _ p
          λw. imOp _ _ _ _ _ (toImMap _ _ _ _ p (class a)) w
          sym _ _ (toImCls _ _ _ _ p b) ⟩
          imOp _ _ _ _ _ (toImMap _ _ _ _ p (class a)) (toImMap _ _ _ _ p (class b))
      v
    u

imopIsImOp : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u v : Im _ _ _ _ p)
  → gop (imIsGroup _ _ _ _ p) u v ≡ imOp _ _ _ _ _ u v
  using (Algebra.groupTheory.gop.eq, imIsGroup.eq)
imopIsImOp = λG g H h p u v. ⋆

toImLaw : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u v : QGroup _ g (ker _ _ _ _ p))
  → toImMap _ _ _ _ _ (gop (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) u v)
    ≡ gop (imIsGroup _ _ _ _ p) (toImMap _ _ _ _ _ u) (toImMap _ _ _ _ _ v)
toImLaw =
  λG g H h p u v. trans
    _
    _
    _
    cong
      λw. Im _ _ _ _ p
      λw. toImMap _ _ _ _ _ w
      qopIsQMul _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p) u v
    trans
      toImMap _ _ _ _ _ (qMul _ _ _ (kerIsNormal _ _ _ _ p) u v)
      _
      _
      toImLawQ
      sym _ _ (imopIsImOp _ _ _ _ _ (toImMap _ _ _ _ _ u) (toImMap _ _ _ _ _ v))

toIm : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  → Hom (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) (imIsGroup _ _ _ _ p)
toIm = λG g H h p. homIntro (toImMap _ _ _ _ p) (toImLaw _ _ _ _ p)

-- ===== im p → G/ker p : THE SHOWCASE =====
--
-- Here is why the image had to be defined with the bracket. To send an
-- element of the image back into the quotient one needs a PREIMAGE,
-- as data, and brElim supplies it. What it charges in exchange is
-- fromImConst — and fromImConst is not overhead, it IS the first
-- isomorphism theorem:
--
--   any two preimages of the same y are congruent modulo ker p.
--
-- Two lines: p (x · x'⁻¹) = p x · (p x')⁻¹ = y · y⁻¹ = e. The content
-- is paid exactly where it is used. With ∥·∥ in place of Br there
-- would be no obligation to pay and no map to define — squash-elim
-- reaches only propositions, and this one lands in data.
fromImConst : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (y : H)
  (f f' : imFib _ _ _ _ p y)
  → qcls g (ker _ _ _ _ p) (f .π₁) ≡ qcls _ _ (f' .π₁)
  using (ker.eq, Algebra.subgroup.cosetRel.eq, imFib.unfold)
fromImConst =
  λG g H h p y f f'. qclsEq
    kerIsSubgroup _ _ _ _ p
    _
    _
    homAp p (gop g (f .π₁) (ginv g (f' .π₁)))
      ≡⟨ homOpInv p (f .π₁) (f' .π₁) ⟩ gop h (homAp p (f .π₁)) (ginv h (homAp p (f' .π₁)))
      ≡⟨ cong (λw. H) (λw. gop h w (ginv h (homAp p (f' .π₁)))) (idToEq _ _ _ (f .π₂)) ⟩
        gop h y (ginv h (homAp p (f' .π₁)))
      ≡⟨ cong (λw. H) (λw. gop h y (ginv h w)) (idToEq _ _ _ (f' .π₂)) ⟩ gop h y (ginv h y)
      ≡⟨ gInvR h y ⟩ ge h

fromImAt : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  (y : H)
  (w : Br (imFib _ _ _ _ p y))
  → QGroup _ g (ker _ _ _ _ p)
  using (imFib.unfold)
fromImAt = λG g H h p y w. brElim (λf. qcls g (ker _ _ _ _ p) (f .π₁)) (fromImConst _ _ _ _ p y) w

fromIm : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  (z : Im _ _ _ _ p)
  → QGroup _ g (ker _ _ _ _ p)
  using (Im.unfold)
fromIm = λG g H h p z. fromImAt _ (z .π₂)

-- ===== the two round trips =====
fromImIn : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {a : G}
  → fromIm (imIn _ _ _ _ p a) ≡ qcls _ _ a
  using (imIn.eq, fromIm.eq, fromImAt.eq, Core.bracket.br.eq, Core.bracket.brElim.eq)
fromImIn = λG g H h p a. ⋆

fromImToIm : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u : QGroup _ g (ker _ _ _ _ p))
  → fromIm (toImMap _ _ _ _ _ u) ≡ u
  using (Algebra.quotGroup.QGroup.unfold, Algebra.quotGroup.qcls.eq)
fromImToIm =
  λG g H h p u. quot-elim
    a. trans
      _
      _
      _
      cong (λw. QGroup _ g (ker _ _ _ _ p)) (λw. fromIm w) (toImCls _ _ _ _ p a)
      fromImIn
    u

-- the other round trip, through imEq: only the H-component has to be
-- checked, and a quot-elim over the bracket recovers the preimage's
-- own Id proof to check it with
toImFromImFst : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (y : H)
  (w : Br (imFib _ _ _ _ p y))
  → toImMap _ _ _ _ _ (fromImAt _ w) .π₁ ≡ y
  using (Im.unfold,
    imFib.unfold,
    imIn.eq,
    fromImAt.eq,
    Core.bracket.Br.unfold,
    Core.bracket.brElim.eq,
    Algebra.quotGroup.qcls.eq)
toImFromImFst =
  λG g H h p y w. quot-elim
    f. trans
      _
      homAp p (f .π₁)
      _
      cong
        λw. H
        λw. w .π₁
        {toImMap G g H h p (fromImAt y (class f))}
        {imIn _ _ _ _ p (f .π₁)}
        toImCls _ _ _ _ p (f .π₁)
      idToEq _ _ _ (f .π₂)
    w

toImFromIm : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (z : Im _ _ _ _ p)
  → toImMap _ _ _ _ _ (fromIm z) ≡ z
  using (Im.unfold, fromIm.eq)
toImFromIm = λG g H h p z. imEq _ _ _ _ _ _ _ (toImFromImFst _ _ _ _ _ _ (z .π₂))

-- ===== the canonical factorisation  p = incl ∘ φ ∘ π  =====
imIncFun : (G : 𝕌) (g : IsGroup G) (H : 𝕌) (h : IsGroup H) (p : Hom g h) (u : Im _ _ _ _ p) → H
  using (Im.unfold)
imIncFun = λG g H h p u. u .π₁

imIncLaw : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u v : Im _ _ _ _ p)
  → imIncFun _ _ _ _ _ (gop (imIsGroup _ _ _ _ p) u v)
    ≡ gop h (imIncFun _ _ _ _ _ u) (imIncFun _ _ _ _ _ v)
  using (imIncFun.eq, imOp.eq)
imIncLaw =
  λG g H h p u v. trans _ _ _ (cong (λw. H) (λw. imIncFun _ _ _ _ _ w) (imopIsImOp _ _ _ _ _ u v)) ⋆

imInc : {G : 𝕌} {g : IsGroup G} {H : 𝕌} {h : IsGroup H} {p : Hom g h} → Hom (imIsGroup _ _ _ _ p) h
imInc = λG g H h p. homIntro (imIncFun _ _ _ _ p) (imIncLaw _ _ _ _ p)

imIncAp : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (u : Im _ _ _ _ p)
  → homAp {} _ (imIsGroup _ _ _ _ p) _ h imInc u ≡ imIncFun _ _ _ _ _ u
  using (imInc.eq)
imIncAp = λG g H h p u. homIntroAp {} _ _ _ _ (imIncFun _ _ _ _ p) (imIncLaw _ _ _ _ p) u

toImAp : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {u : QGroup _ g (ker _ _ _ _ p)}
  → homAp {}
    _
    qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
    _
    imIsGroup _ _ _ _ p
    toIm
    u
    ≡ toImMap _ _ _ _ _ u
  using (toIm.eq)
toImAp = λG g H h p u. homIntroAp {} _ _ _ _ (toImMap _ _ _ _ p) (toImLaw _ _ _ _ p) u

-- φ ∘ π is p, followed into the image
toImOfProj : {G : 𝕌}
  {g : IsGroup G}
  {H : 𝕌}
  {h : IsGroup H}
  {p : Hom g h}
  {a : G}
  → homAp {}
    _
    qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
    _
    imIsGroup _ _ _ _ p
    toIm
    homAp {} _ g _ (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) qProj a
    ≡ imIn _ _ _ _ _ a
  using (Algebra.quotGroup.qcls.eq)
toImOfProj =
  λG g H h p a. trans
    _
    _
    _
    cong
      λw. Im _ _ _ _ p
      λw. homAp {}
        _
        qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
        Im _ _ _ _ p
        imIsGroup _ _ _ _ p
        toIm
        w
      {homAp {} _ g _ (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) qProj a}
      {qcls g (ker _ _ _ _ p) a}
      qProjAp
    trans
      homAp {}
        _
        qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
        _
        imIsGroup _ _ _ _ p
        toIm
        qcls g (ker _ _ _ _ p) a
      toImMap _ _ _ _ _ (qcls g (ker _ _ _ _ p) a)
      _
      toImAp
      toImCls _ _ _ _ p a

-- ...and the inclusion sends it back to p a: the factorisation, closed
firstIsoFactors : (G : 𝕌)
  (g : IsGroup G)
  (H : 𝕌)
  (h : IsGroup H)
  (p : Hom g h)
  (a : G)
  → homAp {}
    _
    imIsGroup _ _ _ _ p
    _
    h
    imInc
    homAp {}
      _
      qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
      _
      imIsGroup _ _ _ _ p
      toIm
      homAp {} _ g _ (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) qProj a
    ≡ homAp p a
  using (imIn.eq, imIncFun.eq)
firstIsoFactors =
  λG g H h p a. trans
    _
    _
    _
    cong
      λw. H
      λw. homAp {} _ (imIsGroup _ _ _ _ p) H h imInc w
      {homAp {}
        _
        qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)
        _
        imIsGroup _ _ _ _ p
        toIm
        homAp {} _ g _ (qIsGroup _ _ _ (kerIsSubgroup _ _ _ _ p) (kerIsNormal _ _ _ _ p)) qProj a}
      {imIn _ _ _ _ p a}
      toImOfProj
    imIncAp _ _ _ _ _ (imIn _ _ _ _ p a)