{- Abstract Algbera:
   - Monoid and CMonoid;
   - Group and AbGroup;
   - Ring and AbRing;
   - Hom sequence;
   - Subgroups, Normal, Full;
   - Presheaf Type Theory.
   Copyright (c) Groupoid Infinity, 2017-1018.

   HoTT 6.11 Algebra -}

-- Original Author: Linus Börjesson.

module algebra where
import pi
import set
import iso_sigma
import quotient

isAssociative (M: U) (op: M -> M -> M): U
  = (a b c: M) -> Path M (op a (op b c)) (op (op a b) c)

propisAssociative (M: U) (sM: isSet M) (op: M -> M -> M)
  : isProp (isAssociative M op)
  = propPi3 M B h where
    B (a b c: M): U = Path M (op a (op b c)) (op (op a b) c)
    h (a b c: M): isProp (B a b c) = sM (op a (op b c)) (op (op a b) c)

hasLeftIdentity (M: U) (op: M -> M -> M) (id: M): U
  = (x: M) -> Path M (op id x) x

prophasLeftIdentity (M: U) (sM: isSet M) (op: M -> M -> M) (id: M)
  : isProp (hasLeftIdentity M op id)
  = propPi M B h where
    B (x: M): U = Path M (op id x) x
    h (x: M): isProp (B x) = sM (op id x) x

hasRightIdentity (M: U) (op: M -> M -> M) (id: M): U
  = (x: M) -> Path M (op x id) x

prophasRightIdentity (M: U) (sM: isSet M) (op: M -> M -> M) (id: M)
  : isProp (hasRightIdentity M op id)
  = propPi M B h where
    B (x: M): U = Path M (op x id) x
    h (x: M): isProp (B x) = sM (op x id) x

hasIdentity (M: U) (op: M -> M -> M) (id: M): U
  = (_: hasLeftIdentity M op id)
  * (hasRightIdentity M op id)

prophasIdentity (M: U) (sM: isSet M) (op: M -> M -> M) (id: M)
  : isProp (hasIdentity M op id)
  = propAnd (hasLeftIdentity M op id)
            (hasRightIdentity M op id)
            (prophasLeftIdentity M sM op id)
            (prophasRightIdentity M sM op id)

isCommutative (M: U) (opx: M -> M -> M): U
  = (x y: M) -> Path M (opx x y) (opx y x)

propisCommutative (M: U) (sM: isSet M) (opx: M -> M -> M)
  : isProp (isCommutative M opx)
  = propPi2 M B h where
    B (x y: M): U = Path M (opx x y) (opx y x)
    h (x y: M): isProp (B x y) = sM (opx x y) (opx y x)

isLeftCancellative (M: U) (opx: M -> M -> M): U
  = (c x y: M) -> Path M (opx c x) (opx c y) -> Path M x y

propisLeftCancellative (M: U) (sM: isSet M) (op: M -> M -> M)
  : isProp (isLeftCancellative M op)
  = propPi3 M B h where
    B0 (c x y: M) (p: Path M (op c x) (op c y)): U = Path M x y
    h0 (c x y: M) (p: Path M (op c x) (op c y)): isProp (B0 c x y p) = sM x y
    B  (c x y: M): U = Path M (op c x) (op c y) -> Path M x y
    h  (c x y: M): isProp (B c x y) = propPi (Path M (op c x) (op c y)) (B0 c x y) (h0 c x y)

isRightCancellative (M: U) (op: M -> M -> M): U
  = (c x y: M) -> Path M (op x c) (op y c) -> Path M x y

propisRightCancellative (M: U) (sM: isSet M) (op: M -> M -> M)
  : isProp (isRightCancellative M op)
  = propPi3 M B h where
    B0 (c x y: M) (p: Path M (op x c) (op y c)): U = Path M x y
    h0 (c x y: M) (p: Path M (op x c) (op y c)): isProp (B0 c x y p) = sM x y
    B  (c x y: M): U = Path M (op x c) (op y c) -> Path M x y
    h  (c x y: M): isProp (B c x y) = propPi (Path M (op x c) (op y c)) (B0 c x y) (h0 c x y)

isCancellative (M: U) (op: M -> M -> M): U
  = (_: isLeftCancellative M op)
  * (isRightCancellative M op)

propisCancellative (M: U) (sM: isSet M) (op: M -> M -> M)
  : isProp (isCancellative M op)
  = propAnd (isLeftCancellative M op)
            (isRightCancellative M op)
            (propisLeftCancellative M sM op)
            (propisRightCancellative M sM op)

hasLeftInverse (G: U) (op: G -> G -> G) (id: G) (inv: G -> G): U
  = (x: G) -> Path G (op (inv x) x) id

prophasLeftInverse (G: U) (sG: isSet G) (op: G -> G -> G) (id: G) (inv: G -> G)
  : isProp (hasLeftInverse G op id inv)
  = propPi G B h where
    B (x: G): U = Path G (op (inv x) x) id
    h (x: G): isProp (B x) = sG (op (inv x) x) id

hasRightInverse (G: U) (op: G -> G -> G) (id: G) (inv: G -> G): U
  = (x: G) -> Path G (op x (inv x)) id

prophasRightInverse (G: U) (sG: isSet G) (op: G -> G -> G) (id: G) (inv: G -> G)
  : isProp (hasRightInverse G op id inv)
  = propPi G B h where
    B (x: G): U = Path G (op x (inv x)) id
    h (x: G): isProp (B x) = sG (op x (inv x)) id

hasInverse (G: U) (op: G -> G -> G) (id: G) (inv: G -> G): U
  = (_: hasLeftInverse G op id inv)
  * (hasRightInverse G op id inv)

prophasInverse (G: U) (sG: isSet G) (op: G -> G -> G) (id: G) (inv: G -> G)
  : isProp (hasInverse G op id inv)
  = propAnd (hasLeftInverse G op id inv)
            (hasRightInverse G op id inv)
            (prophasLeftInverse G sG op id inv)
            (prophasRightInverse G sG op id inv)

isLeftDistributive (R: U) (add: R -> R -> R) (mul: R -> R -> R): U
  = (a b c: R) -> Path R (mul a (add b c)) (add (mul a b) (mul a c))

propisLeftDistributive (R: U) (sR: isSet R) (add: R -> R -> R) (mul: R -> R -> R)
  : isProp (isLeftDistributive R add mul)
  = propPi3 R B h where
    B (a b c: R): U = Path R (mul a (add b c)) (add (mul a b) (mul a c))
    h (a b c: R): isProp (B a b c) = sR (mul a (add b c)) (add (mul a b) (mul a c))

isRightDistributive (R: U) (add: R -> R -> R) (mul: R -> R -> R): U
  = (a b c: R) -> Path R (mul (add b c) a) (add (mul b a) (mul c a))

propisRightDistributive (R: U) (sR: isSet R) (add: R -> R -> R) (mul: R -> R -> R)
  : isProp (isRightDistributive R add mul)
  = propPi3 R B h where
    B (a b c: R): U = Path R (mul (add b c) a) (add (mul b a) (mul c a))
    h (a b c: R): isProp (B a b c) = sR (mul (add b c) a) (add (mul b a) (mul c a))

isDistributive (R: U) (add: R -> R -> R) (mul: R -> R -> R): U
  = (_: isLeftDistributive R add mul)
  * (isRightDistributive R add mul)

propisDistributive (R: U) (sR: isSet R) (add: R -> R -> R) (mul: R -> R -> R)
  : isProp (isDistributive R add mul)
  = propAnd (isLeftDistributive R add mul)
            (isRightDistributive R add mul)
            (propisLeftDistributive R sR add mul)
            (propisRightDistributive R sR add mul)

preservesOp (A B: U) (oA: A -> A -> A) (oB: B -> B -> B) (f: A -> B): U
  = (a0 a1: A) -> Path B (f (oA a0 a1)) (oB (f a0) (f a1))

proppreservesOp (A B: U) (sB: isSet B) (oA: A -> A -> A) (oB: B -> B -> B)
    (f: A -> B): isProp (preservesOp A B oA oB f)
  = propPi2 A (\(a0 a1: A) -> Path B (f (oA a0 a1)) (oB (f a0) (f a1)))
              (\(a0 a1: A) -> sB (f (oA a0 a1)) (oB (f a0) (f a1)))

preservesId (A B: U) (iA: A) (iB: B) (f: A -> B): U
  = Path B (f iA) iB

proppreservesId (A B: U) (sB: isSet B) (iA: A) (iB: B) (f: A -> B)
  : isProp (preservesId A B iA iB f)
  = sB (f iA) iB

-- Structures

isMonoid (M: SET): U
  = (op: M.1 -> M.1 -> M.1)
  * (assoc: isAssociative M.1 op)
  * (id: M.1)
  * (hasIdentity M.1 op id)

isGroup (G: SET): U
  = (m: isMonoid G)
  * (inv: G.1 -> G.1)
  * (hasInverse G.1 m.1 m.2.2.1 inv)

isDifferentialGroup (G: SET): U
  = (g: isGroup G)
  * (comm: isCommutative G.1 g.1.1)
  * (boundary: G.1 -> G.1)
  * ((x: G.1) -> Path G.1 (boundary (boundary x)) g.1.2.2.1)

isCMonoid (M: SET): U
  = (m: isMonoid M)
  * (isCommutative M.1 m.1)

isAbGroup (G: SET): U
  = (g: isGroup G)
  * (isCommutative G.1 g.1.1)

isRing (R: SET): U
  = (mul: isMonoid R)
  * (add: isAbGroup R)
  * (isDistributive R.1 add.1.1.1 mul.1)

isAbRing (R: SET): U
  = (mul: isCMonoid R)
  * (add: isAbGroup R)
  * (isDistributive R.1 add.1.1.1 mul.1.1)


monoid:  U = (X: SET) * isMonoid X
cmonoid: U = (X: SET) * isCMonoid X
group:   U = (X: SET) * isGroup X
abgroup: U = (X: SET) * isAbGroup X
ring:    U = (X: SET) * isRing X
abring:  U = (X: SET) * isAbRing X
dgroup:  U = (X: SET) * isDifferentialGroup X

-- Unit Abelian Group
unitAbGroup: abgroup
  = ((unit,setUnit),(((op,asso,id,(lx,rx)),inv,(li,ri)),comm)) where
    op: unit -> unit -> unit = \(x y: unit) -> y
    id: unit = tt
    inv: unit -> unit = \(x: unit) -> tt
    lx: (x: unit) -> Path unit (op id x) x = \(x: unit) -> <i> (op id x)
    rx: (x: unit) -> Path unit (op x id) x = split tt -> <i> tt
    li: (x: unit) -> Path unit (op (inv x) x) id = split tt -> <i> tt
    ri: (x: unit) -> Path unit (op x (inv x)) id = split tt -> <i> tt
    asso: isAssociative unit op = split tt -> \(x y: unit) -> <i> y
    comm: isCommutative unit op = split tt -> \(x: unit) -> <i> rx x @ -i

-- Accessors
opMonoid       (m: monoid): m.1.1 -> m.1.1 -> m.1.1 = m.2.1
isAssocMonoid  (m: monoid): isAssociative m.1.1 (opMonoid m) = m.2.2.1
idMonoid       (m: monoid): m.1.1 = m.2.2.2.1
hasIdMonoid    (m: monoid): hasIdentity m.1.1 (opMonoid m) (idMonoid m) = m.2.2.2.2

-- Commutative monoids
opCMonoid      (m: cmonoid): m.1.1 -> m.1.1 -> m.1.1 = m.2.1.1
isAssocCMonoid (m: cmonoid): isAssociative m.1.1 (opCMonoid m) = m.2.1.2.1
idCMonoid      (m: cmonoid): m.1.1 = m.2.1.2.2.1
hasIdCMonoid   (m: cmonoid): hasIdentity m.1.1 (opCMonoid m) (idCMonoid m) = m.2.1.2.2.2
isCommCMonoid  (m: cmonoid): isCommutative m.1.1 (opCMonoid m) = m.2.2

-- Groups
opGroup       (g: group): g.1.1 -> g.1.1 -> g.1.1 = g.2.1.1
isAssocGroup  (g: group): isAssociative g.1.1 (opGroup g) = g.2.1.2.1
idGroup       (g: group): g.1.1 = g.2.1.2.2.1
hasIdGroup    (g: group): hasIdentity g.1.1 (opGroup g) (idGroup g) = g.2.1.2.2.2
invGroup      (g: group): g.1.1 -> g.1.1 = g.2.2.1
hasInvGroup   (g: group): hasInverse g.1.1 (opGroup g) (idGroup g) (invGroup g) = g.2.2.2

-- Commutative groups
opCGroup      (g: abgroup): g.1.1 -> g.1.1 -> g.1.1 = g.2.1.1.1
isAssocCGroup (g: abgroup): isAssociative g.1.1 (opCGroup g) = g.2.1.1.2.1
idCGroup      (g: abgroup): g.1.1 = g.2.1.1.2.2.1
hasIdCGroup   (g: abgroup): hasIdentity g.1.1 (opCGroup g) (idCGroup g) = g.2.1.1.2.2.2
isCommCGroup  (g: abgroup): isCommutative g.1.1 (opCGroup g) = g.2.2
invCGroup     (g: abgroup): g.1.1 -> g.1.1 = g.2.1.2.1
hasInvCGroup  (g: abgroup): hasInverse g.1.1 (opCGroup g) (idCGroup g) (invCGroup g) = g.2.1.2.2

-- Groups are cancellative
lem_group_lcancellative (g: group)
                        (c x y: g.1.1)
                        (p: Path g.1.1 (opGroup g c x) (opGroup g c y)): Path g.1.1 x y
  = <i> comp (<_> g.1.1) (opGroup g (invGroup g c) (p @ i))
             [(i=0) -> <j> comp (<_> g.1.1) (opGroup g ((hasInvGroup g).1 c @ j) x)
                                [(j=0) -> <k> isAssocGroup g (invGroup g c) c x @ -k,
                                 (j=1) -> (hasIdGroup g).1 x ],
              (i=1) -> <j> comp (<_> g.1.1) (opGroup g ((hasInvGroup g).1 c @ j) y)
                                [(j=0) -> <k> isAssocGroup g (invGroup g c) c y @ -k,
                                 (j=1) -> (hasIdGroup g).1 y ] ]

lem_group_rcancellative (g: group) (c x y: g.1.1) (p: Path g.1.1 (opGroup g x c) (opGroup g y c))
  : Path g.1.1 x y
  = <i> comp (<_> g.1.1) (opGroup g (p @ i) (invGroup g c))
    [ (i = 0) -> <j> comp (<_> g.1.1) (opGroup g x ((hasInvGroup g).2 c @ j))
        [ (j = 0) -> isAssocGroup g x c (invGroup g c)
        , (j = 1) -> (hasIdGroup g).2 x ]
    , (i = 1) -> <j> comp (<_> g.1.1) (opGroup g y ((hasInvGroup g).2 c @ j))
        [ (j = 0) -> isAssocGroup g y c (invGroup g c)
        , (j = 1) -> (hasIdGroup g).2 y ] ]

lem_group_cancellative (g: group)
  : isCancellative g.1.1 (opGroup g)
  = (lem_group_lcancellative g, lem_group_rcancellative g)

-- (a · b)⁻¹ = b⁻¹ · a⁻¹
lem_group_inv_dist (g: group) (a b: g.1.1)
  : Path g.1.1 (invGroup g (opGroup g a b)) (opGroup g (invGroup g b) (invGroup g a))
  = let
    a': g.1.1 = invGroup g a
    b': g.1.1 = invGroup g b
    x: g.1.1 = opGroup g a b
    x': g.1.1 = invGroup g (opGroup g a b)
    p0: Path g.1.1 (opGroup g x' a) b'
      = <i> comp (<_> g.1.1) (opGroup g ((hasInvGroup g).1 (opGroup g a b) @ i) b')
        [ (i = 1) -> (hasIdGroup g).1 b'
        , (i = 0) -> <j> comp (<_> g.1.1) (isAssocGroup g x' x b' @ -j)
          [ (j = 0) -> <_> opGroup g (opGroup g x' x) b'
          , (j = 1) -> <k> comp (<_> g.1.1) (opGroup g x' (isAssocGroup g a b b' @ -k))
            [ (k = 0) -> <_> opGroup g x' (opGroup g x b')
            , (k = 1) -> <l> comp (<_> g.1.1)
                              (opGroup g x' (opGroup g a ((hasInvGroup g).2 b @ l)))
              [ (l = 0) -> <_> opGroup g x' (opGroup g a (opGroup g b b'))
              , (l = 1) -> <m> opGroup g x' ((hasIdGroup g).2 a @ m) ]]]] in
  <i> comp (<_> g.1.1) (opGroup g (p0 @ i) a')
           [ (i = 1) -> <_> opGroup g b' a'
           , (i = 0) -> <j> comp (<_> g.1.1) (isAssocGroup g x' a a' @ -j)
             [ (j = 0) -> <_> opGroup g (opGroup g x' a) a'
             , (j = 1) -> <k> comp (<_> g.1.1) (opGroup g x' ((hasInvGroup g).2 a @ k))
               [ (k = 0) -> <_> opGroup g x' (opGroup g a a')
               , (k = 1) -> (hasIdGroup g).2 x' ]]]

-- a⁻¹ · b⁻¹ = (a · b)⁻¹
lem_cgroup_inv_dist (g: abgroup) (a b: g.1.1)
  : Path g.1.1 (opCGroup g (invCGroup g a) (invCGroup g b)) (invCGroup g (opCGroup g a b))
  = <i> comp (<_> g.1.1) (lem_group_inv_dist (g.1, g.2.1) a b @ -i)
    [ (i = 0) -> isCommCGroup g (invCGroup g b) (invCGroup g a)
    , (i = 1) -> <_> invCGroup g (opCGroup g a b) ]

-- e⁻¹ = e
lemma_group_inv_id (g : group)
  : Path g.1.1 (invGroup g (idGroup g)) (idGroup g)
  = <i> comp (<_> g.1.1) ((hasIdGroup g).2 (invGroup g (idGroup g)) @ -i)
    [ (i = 0) -> <_> invGroup g (idGroup g)
    , (i = 1) -> (hasInvGroup g).1 (idGroup g) ]

-- e⁻¹ = e (abelian groups)
lemma_cgroup_inv_id (g: abgroup)
  : Path g.1.1 (invCGroup g (idCGroup g)) (idCGroup g)
  = lemma_group_inv_id (g.1, g.2.1)

-- x⁻¹⁻¹ = x⁻¹⁻¹ * 1 = x⁻¹⁻¹ * (x⁻¹ * x) = (x⁻¹⁻¹ * x⁻¹) * x = 1 * x = x
invInvGroup (G : group) (x : G.1.1) : Path G.1.1 (invGroup G (invGroup G x)) x =
  <i> comp (<_> G.1.1) (lem @ i)
           [ (i = 0) -> (hasIdGroup G).2 (inv (inv x))
           , (i = 1) -> (hasIdGroup G).1 x ]
  where
    op (a b : G.1.1) : G.1.1 = opGroup G a b
    inv (a : G.1.1) : G.1.1 = invGroup G a
    e : G.1.1 = idGroup G
    lem : Path G.1.1 (op (inv (inv x)) e) (op e x)
      = <i> comp (<_> G.1.1) (isAssocGroup G (inv (inv x)) (inv x) x @ i)
                 [ (i = 0) -> <j> op (inv (inv x)) ((hasInvGroup G).1 x @ j)
                 , (i = 1) -> <j> op ((hasInvGroup G).1 (inv x) @ j) x ]

-- Homomorphisms

-- The monoid homomorphism preserves both the structure and the identity element
ismonoidhom (a b: monoid) (f: a.1.1 -> b.1.1): U
  = (_: preservesOp a.1.1 b.1.1 (opMonoid a) (opMonoid b) f)
  * (preservesId a.1.1 b.1.1 (idMonoid a) (idMonoid b) f)

propismonoidhom (a b: monoid) (f: a.1.1 -> b.1.1)
  : isProp (ismonoidhom a b f)
  = propAnd (preservesOp a.1.1 b.1.1 (opMonoid a) (opMonoid b) f)
            (preservesId a.1.1 b.1.1 (idMonoid a) (idMonoid b) f)
            (proppreservesOp a.1.1 b.1.1 b.1.2 (opMonoid a) (opMonoid b) f)
            (proppreservesId a.1.1 b.1.1 b.1.2 (idMonoid a) (idMonoid b) f)

monoidhom (a b: monoid): U
  = (f: a.1.1 -> b.1.1)
  * (ismonoidhom a b f)

-- Homomorphisms between underlying monoids
cmonoidhom   (a b: cmonoid): U = monoidhom (a.1, a.2.1)   (b.1, b.2.1)
grouphom     (a b: group):   U = monoidhom (a.1, a.2.1)   (b.1, b.2.1)
abgrouphom   (a b: abgroup): U = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1)
dgrouphom    (a b: dgroup):  U = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1)
cmonabgrouphom (a: cmonoid) (b: abgroup): U = monoidhom (a.1, a.2.1) (b.1, b.2.1.1)

-- Homomorphism constructors
group' (g : group) : monoid = (g.1, g.2.1)
grouphom' (a b: group) (f: a.1.1 -> b.1.1)
          (pO: preservesOp a.1.1 b.1.1 (opGroup a) (opGroup b) f)
  : monoidhom (group' a) (group' b)
  = (f,pO,(lem_group_cancellative b).1(f(idGroup a))(f(idGroup a))(idGroup b)p) where
    p: Path b.1.1(opGroup b(f(idGroup a))(f(idGroup a)))(opGroup b (f(idGroup a))(idGroup b))
      = <i> comp (<_> b.1.1) (f ((hasIdGroup a).1 (idGroup a) @ i))
        [ (i = 0) -> pO (idGroup a) (idGroup a),
          (i = 1) -> <j> (hasIdGroup b).2 (f (idGroup a)) @ -j ]

abgroup' (a : abgroup) : group = (a.1, a.2.1)
abgrouphom' (a b: abgroup) (f: a.1.1 -> b.1.1)
    (pO: preservesOp a.1.1 b.1.1 (opCGroup a) (opCGroup b) f)
  : monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1)
  = grouphom' (abgroup' a) (abgroup' b) f pO

-- g ∘ f
monoidhomcomp (a b c: monoid)
    (f: monoidhom a b) (g: monoidhom b c)
  : monoidhom a c
  = (h, pO, pI) where
    h (x: a.1.1): c.1.1 = g.1 (f.1 x)
    pO (x0 x1: a.1.1): Path c.1.1 (h (a.2.1 x0 x1)) (c.2.1 (h x0) (h x1))
      = <i> comp (<_> c.1.1) (g.1 (f.2.1 x0 x1 @ i))
        [ (i = 0) -> <_> h (a.2.1 x0 x1)
        , (i = 1) -> g.2.1 (f.1 x0) (f.1 x1) ]
    pI: Path c.1.1 (h (idMonoid a)) (idMonoid c)
      = <i> comp (<_> c.1.1) (g.1 (f.2.2 @ i))
        [ (i = 0) -> <_> h (idMonoid a)
        , (i = 1) -> g.2.2 ]

grouphomcomp (a b c : group)
  (f : grouphom a b) (g : grouphom b c) : grouphom a c
  = monoidhomcomp (group' a) (group' b) (group' c) f g

abgrouphomcomp (a b c : abgroup)
  (f : abgrouphom a b) (g : abgrouphom b c) : abgrouphom a c
  = monoidhomcomp (group' (abgroup' a)) (group' (abgroup' b)) (group' (abgroup' c)) f g

-- h ∘ (g ∘ f) = (h ∘ g) ∘ f
lemma_monoidcomp0 (a b c d: monoid) (f: monoidhom a b)
    (g: monoidhom b c) (h: monoidhom c d)
  : Path (monoidhom a d) (monoidhomcomp a c d (monoidhomcomp a b c f g) h)
                         (monoidhomcomp a b d f (monoidhomcomp b c d g h))
  = lemSig (a.1.1 -> d.1.1) (ismonoidhom a d) (propismonoidhom a d) f0 f1 (<_> f0.1) where
    f0: monoidhom a d = monoidhomcomp a c d (monoidhomcomp a b c f g) h
    f1: monoidhom a d = monoidhomcomp a b d f (monoidhomcomp b c d g h)

trivmonoidhom (a b : monoid) : monoidhom a b
  = (\(x : a.1.1) -> idMonoid b, \(x y : a.1.1) -> <i> (hasIdMonoid b).1 (idMonoid b) @ -i, <_> idMonoid b)

trivabgrouphom (a b : abgroup) : abgrouphom a b
  = trivmonoidhom (group' (abgroup' a)) (group' (abgroup' b))

-- 1_a
idmonoidhom (a: monoid): monoidhom a a
  = (\ (x: a.1.1) -> x, \(a0 a1: a.1.1) -> <_> opMonoid a a0 a1, <_> idMonoid a)

-- f ∘ 1_a = f
lemma_idmonoidhom0 (a b: monoid) (f: monoidhom a b)
  : Path (monoidhom a b) (monoidhomcomp a a b (idmonoidhom a) f) f
  = lemSig (a.1.1 -> b.1.1) (ismonoidhom a b) (propismonoidhom a b) h f (<_> f.1) where
    h: monoidhom a b = monoidhomcomp a a b (idmonoidhom a) f

-- 1_b ∘ f = f
lemma_idmonoidhom1 (a b: monoid) (f: monoidhom a b)
  : Path (monoidhom a b) (monoidhomcomp a b b f (idmonoidhom b)) f
  = lemSig (a.1.1 -> b.1.1) (ismonoidhom a b) (propismonoidhom a b) h f (<_> f.1) where
    h: monoidhom a b = monoidhomcomp a b b f (idmonoidhom b)

-- f(x⁻¹) = f(x)⁻¹
lem_grouphom_inv (g h: group) (f: grouphom g h) (x: g.1.1)
  : Path h.1.1 (f.1 (invGroup g x)) (invGroup h (f.1 x))
  = <i> comp (<_> h.1.1) (p2 @ i) [(i=0) -> (hasIdGroup h).1 (f.1 x'), (i=1) -> <_> y' ] where
    x': g.1.1 = invGroup g x
    y: h.1.1 = f.1 x
    y': h.1.1 = invGroup h y
    p0: Path h.1.1 (opGroup h y (f.1 x')) (idGroup h)
        = <i> comp (<_> h.1.1) (f.1 ((g.2.2.2).2 x @ i)) [(i=0) -> f.2.1 x x', (i=1) -> f.2.2 ]
    p1: Path h.1.1 (opGroup h (opGroup h y' y) (f.1 x')) y'
        = <i> comp (<_> h.1.1) (opGroup h y' (p0 @ i)) [(i=0) -> isAssocGroup h y' y (f.1 x'),
                                                          (i=1) -> (hasIdGroup h).2 y' ]
    p2: Path h.1.1 (opGroup h (idGroup h) (f.1 x')) y'
        = <i> comp (<_> h.1.1) (p1 @ i) [(i=0) -> <j> opGroup h ((h.2.2.2).1 y @ j) (f.1 x'),
                                         (i=1) -> <_> y' ]

subtypeEquality (A: U) (B: A -> U) (pB: (x : A) -> isProp (B x)) (s t: Sigma A B)
  : Path A s.1 t.1 -> Path (Sigma A B) s t
  = trans (Path A s.1 t.1) (Path (Sigma A B) s t) (<i> lemSigProp A B pB s t @ -i)

ldiv (H: group) (g h: H.1.1) : H.1.1
  = (opGroup H) ((invGroup H) g) h

rdiv (H: group) (g h: H.1.1) : H.1.1
  = (opGroup H) g ((invGroup H) h)

conjugate (G: group) (g1 g2: G.1.1): G.1.1
   = rdiv G ((opGroup G) g1 g2) g1

subtypeProp (A: U): U
  = (P : A -> U)
  * (a : A) -> isProp (P a)

subtype (A : U) (P : subtypeProp A): U
  = (x : A) -- prop
  * (P.1 x) -- level

subgroupProp (G: group): U
  = (prop: G.1.1 -> U)
  * (level: (x: G.1.1) -> isProp (prop x))
  * (ident: prop (idGroup G))
  * (inv: (g: G.1.1) -> prop g -> prop ((invGroup G) g))
  * ((g1 g2: G.1.1) -> prop g1 -> prop g2 -> prop ((opGroup G) g1 g2))

-- Accessors
subgroupLevel (G : group) (P : subgroupProp G) : (x : G.1.1) -> isProp (P.1 x) = P.2.1
subgroupId    (G : group) (P : subgroupProp G) : P.1 (idGroup G) = P.2.2.1
subgroupInv   (G : group) (P : subgroupProp G) : (g: G.1.1) -> P.1 g -> P.1 ((invGroup G) g) = P.2.2.2.1
subgroupOp    (G : group) (P : subgroupProp G) : (g1 g2: G.1.1) -> P.1 g1 -> P.1 g2 -> P.1 ((opGroup G) g1 g2) = P.2.2.2.2

subgroupPropRdiv (G : group) (P : subgroupProp G) (g1 g2 : G.1.1)
  (u : P.1 g1) (v : P.1 g2) : P.1 (rdiv G g1 g2)
  = subgroupOp G P g1 ((invGroup G) g2) u (subgroupInv G P g2 v)

subgroupSelfRdiv (G : group) (P : subgroupProp G) (g : G.1.1) : P.1 (rdiv G g g)
  = transport (<i> P.1 ((hasInvGroup G).2 g @ -i)) (subgroupId G P)

isNormal (G: group) (P: subgroupProp G) : U
  = (X: group)
  * (g1 g2: G.1.1) -> P.1 g2 -> P.1 (conjugate G g1 g2)

isFull (G: group) (P: subgroupProp G): U
  = (g: G.1.1) -> P.1 g

normalSubgroupProp (G: group): U
  = (P: subgroupProp G)
  * isNormal G P

subElProp (G: group) (P: subgroupProp G)
  : subtypeProp G.1.1
  = (P.1,P.2.1)

subEl (G: group) (P: subgroupProp G): U
  = subtype G.1.1 (subElProp G P)

isSetSubEl (G: group) (P: subgroupProp G): isSet (subEl G P)
  = setSig G.1.1 P.1 G.1.2 (\(x : G.1.1) -> propSet (P.1 x) (P.2.1 x))

subgroup (G: group) (P: subgroupProp G): group
  = ((subEl G P, isSetSubEl G P), ((op, assoc, id, (lx, rx)), inv, (li, ri))) where
    un: U = subEl G P
    op (x y: un): un = ((opGroup G) x.1 y.1, subgroupOp G P x.1 y.1 x.2 y.2)
    unPath (x y : un) (p : Path G.1.1 x.1 y.1) : Path un x y = subtypeEquality G.1.1 P.1 P.2.1 x y p
    assoc: isAssociative un op = \(x y z : un) -> unPath (op x (op y z)) (op (op x y) z) ((isAssocGroup G) x.1 y.1 z.1)
    id: un = ((idGroup G), subgroupId G P)
    lx (x: un): Path un (op id x) x = unPath (op id x) x ((hasIdGroup G).1 x.1)
    rx (x: un): Path un (op x id) x = unPath (op x id) x ((hasIdGroup G).2 x.1)
    inv (x: un): un = ((invGroup G) x.1, subgroupInv G P x.1 x.2)
    li (x: un) : Path un (op (inv x) x) id = unPath (op (inv x) x) id ((hasInvGroup G).1 x.1)
    ri (x: un) : Path un (op x (inv x)) id = unPath (op x (inv x)) id ((hasInvGroup G).2 x.1)

--   a⁻¹ * b
-- = a⁻¹ * b⁻¹⁻¹
-- = (1 * a⁻¹) * b⁻¹⁻¹
-- = ((b⁻¹ * b⁻¹⁻¹) * a⁻¹) * b⁻¹⁻¹
-- = (b⁻¹ * (b⁻¹⁻¹ * a⁻¹)) * b⁻¹⁻¹
-- = (b⁻¹ * (a * b⁻¹)⁻¹) * b⁻¹⁻¹
ldivToConjInvRdiv (G : group) (a b : G.1.1) :
  Path G.1.1 (ldiv G a b) (conjugate G (invGroup G b) (invGroup G (rdiv G a b)))
  = <i> comp (<_> G.1.1) (op ((hasIdGroup G).1 (inv a) @ -i) (inv (inv b)))
             [ (i = 0) -> <j> op (inv a) (invInvGroup G b @ j)
             , (i = 1) -> lem ]
  where
    op (a b : G.1.1) : G.1.1 = opGroup G a b
    inv (a : G.1.1) : G.1.1 = invGroup G a
    e : G.1.1 = idGroup G
    lem : Path G.1.1 (op (op e (inv a)) (inv (inv b)))
                     (conjugate G (inv b) (inv (rdiv G a b)))
      = <i> comp (<_> G.1.1) (op (isAssocGroup G (inv b) (inv (inv b)) (inv a) @ -i) (inv (inv b)))
            [ (i = 0) -> <j> op (op ((hasInvGroup G).2 (inv b) @ j) (inv a)) (inv (inv b))
            , (i = 1) -> <j> op (op (inv b) (lem_group_inv_dist G a (inv b) @ -j)) (inv (inv b)) ]

normalSubgroupLem (G : group) (P : normalSubgroupProp G)
  (a b : G.1.1) (p : P.1.1 (rdiv G a b)) : P.1.1 (opGroup G (invGroup G a) b)
  = transport (<i> P.1.1 (ldivToConjInvRdiv G a b @ -i))
              (P.2.2 (invGroup G b) (invGroup G (rdiv G a b))
                (subgroupInv G P.1 (rdiv G a b) p))

factorProp (G : group) (P : normalSubgroupProp G) : G.1.1 -> G.1.1 -> U
  = \(x y : G.1.1) -> P.1.1 (rdiv G x y)

factor (G : group) (P : normalSubgroupProp G) : U
  = setQuot G.1.1 (factorProp G P)

factorIsSet (G : group) (P : normalSubgroupProp G) : isSet (factor G P)
  = setQuotIsSet G.1.1 (factorProp G P)

factorIncl (G : group) (P : normalSubgroupProp G) (x : G.1.1) : factor G P
  = quotient x

idFactor (G : group) (P : normalSubgroupProp G) : factor G P
  = factorIncl G P (idGroup G)

opFactor (G : group) (P : normalSubgroupProp G) : factor G P -> factor G P -> factor G P
  = setQuotLift2 G.1.1 G.1.1 (factor G P) (factorProp G P) (factorProp G P)
    (subgroupSelfRdiv G P.1) (subgroupSelfRdiv G P.1)
    (factorIsSet G P)
    (\(a b : G.1.1) -> factorIncl G P (op a b))
    (\(a1 b1 a2 b2 : G.1.1) (p : P.1.1 (rdiv G a1 b1)) (q : P.1.1 (rdiv G a2 b2)) ->
      setQuotId G.1.1 (factorProp G P) (op a1 a2) (op b1 b2)
        transport (<i> P.1.1 (lem6 a1 b1 a2 b2 @ -i))
                  (P.2.2 b1 (op (inv (op (inv a1) b1)) (op a2 (inv b2)))
                    (subgroupOp G P.1 (inv (op (inv a1) b1)) (rdiv G a2 b2)
                      (subgroupInv G P.1 (op (inv a1) b1)
                        (normalSubgroupLem G P a1 b1 p)) q)))
  where
    --   ((a1 * a2) * (b1 * b2)⁻¹)                    (A)
    -- = ((a1 * a2) * (b2⁻¹ * b1⁻¹))                     
    -- = 1 * ((a1 * a2) * (b2⁻¹ * b1⁻¹))                 
    -- = (b1 * b1⁻¹) * ((a1 * a2) * (b2⁻¹ * b1⁻¹))    (B)
    -- = b1 * (b1⁻¹ * ((a1 * a2) * (b2⁻¹ * b1⁻¹)))       
    -- = b1 * (b1⁻¹ * (((a1 * a2) * b2⁻¹) * b1⁻¹))       
    -- = b1 * ((b1⁻¹ * ((a1 * a2) * b2⁻¹)) * b1⁻¹)    (C)
    -- = b1 * (((b1⁻¹ * (a1 * a2)) * b2⁻¹) * b1⁻¹)       
    -- = b1 * ((((b1⁻¹ * a1) * a2) * b2⁻¹) * b1⁻¹)       
    -- = b1 * (((b1⁻¹ * a1) * (a2 * b2⁻¹)) * b1⁻¹)    (D)
    -- = b1 * (((b1⁻¹ * a1⁻¹⁻¹) * (a2 * b2⁻¹)) * b1⁻¹)   
    -- = b1 * (((a1⁻¹ * b1)⁻¹ * (a2 * b2⁻¹)) * b1⁻¹)  (E)
    -- = (b1 * ((a1⁻¹ * b1)⁻¹ * (a2 * b2⁻¹))) * b1⁻¹  (F)
    op (a b : G.1.1) : G.1.1 = opGroup G a b
    inv (a : G.1.1) : G.1.1 = invGroup G a
    A (a1 b1 a2 b2 : G.1.1) : G.1.1 = rdiv G (op a1 a2) (op b1 b2)
    B (a1 b1 a2 b2 : G.1.1) : G.1.1 = op (rdiv G b1 b1) (op (op a1 a2) (op (inv b2) (inv b1)))
    C (a1 b1 a2 b2 : G.1.1) : G.1.1 = op b1 (op (op (inv b1) (op (op a1 a2) (inv b2))) (inv b1))
    D (a1 b1 a2 b2 : G.1.1) : G.1.1 = op b1 (op (op (op (inv b1) a1) (op a2 (inv b2))) (inv b1))
    E (a1 b1 a2 b2 : G.1.1) : G.1.1 = op b1 (op (op (inv (op (inv a1) b1)) (op a2 (inv b2))) (inv b1))
    F (a1 b1 a2 b2 : G.1.1) : G.1.1 = op (op b1 (op (inv (op (inv a1) b1)) (op a2 (inv b2)))) (inv b1)
    lem1 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (A a1 b1 a2 b2) (B a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) ((hasIdGroup G).1 (op (op a1 a2) (op (inv b2) (inv b1))) @ -i)
                 [ (i = 0) -> <j> op (op a1 a2) (lem_group_inv_dist G b1 b2 @ -j)
                 , (i = 1) -> <j> op ((hasInvGroup G).2 b1 @ -j) (op (op a1 a2) (op (inv b2) (inv b1))) ]
    lem2 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (B a1 b1 a2 b2) (C a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) (op b1 (op (inv b1) (isAssocGroup G (op a1 a2) (inv b2) (inv b1) @ i)))
                 [ (i = 0) -> isAssocGroup G b1 (inv b1) (op (op a1 a2) (op (inv b2) (inv b1)))
                 , (i = 1) -> <j> op b1 (isAssocGroup G (inv b1) (op (op a1 a2) (inv b2)) (inv b1) @ j) ]
    lem3 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (C a1 b1 a2 b2) (D a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) (op b1 (op (op (isAssocGroup G (inv b1) a1 a2 @ i) (inv b2)) (inv b1)))
                 [ (i = 0) -> <j> op b1 (op (isAssocGroup G (inv b1) (op a1 a2) (inv b2) @ -j) (inv b1))
                 , (i = 1) -> <j> op b1 (op (isAssocGroup G (op (inv b1) a1) a2 (inv b2) @ -j) (inv b1)) ]
    lem4 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (D a1 b1 a2 b2) (A a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) (lem2 a1 b1 a2 b2 @ -i)
                 [ (i = 0) -> lem3 a1 b1 a2 b2
                 , (i = 1) -> <j> lem1 a1 b1 a2 b2 @ -j ]
    lem5 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (A a1 b1 a2 b2) (E a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) (op b1 (op (op (op (inv b1) (invInvGroup G a1 @ -i)) (op a2 (inv b2))) (inv b1)))
                 [ (i = 0) -> lem4 a1 b1 a2 b2
                 , (i = 1) -> <j> op b1 (op (op (lem_group_inv_dist G (inv a1) b1 @ -j) (op a2 (inv b2))) (inv b1)) ]
    lem6 (a1 b1 a2 b2 : G.1.1) : Path G.1.1 (A a1 b1 a2 b2) (F a1 b1 a2 b2)
      = <i> comp (<_> G.1.1) (isAssocGroup G b1 (op (inv (op (inv a1) b1)) (op a2 (inv b2))) (inv b1) @ i)
                 [ (i = 0) -> <j> lem5 a1 b1 a2 b2 @ -j
                 , (i = 1) -> <_> F a1 b1 a2 b2 ]

hasLeftIdFactor (G : group) (P : normalSubgroupProp G) :
  (x : factor G P) -> Path (factor G P) (opFactor G P (idFactor G P) x) x
  = setQuotIndProp G.1.1 (factorProp G P)
    (\(x : factor G P) -> Path (factor G P) (opFactor G P (idFactor G P) x) x)
    (\(x : G.1.1) -> <i> quotient ((hasIdGroup G).1 x @ i))
    (\(x : factor G P) -> factorIsSet G P (opFactor G P (idFactor G P) x) x)

hasRightIdFactor (G : group) (P : normalSubgroupProp G) :
  (x : factor G P) -> Path (factor G P) (opFactor G P x (idFactor G P)) x
  = setQuotIndProp G.1.1 (factorProp G P)
    (\(x : factor G P) -> Path (factor G P) (opFactor G P x (idFactor G P)) x)
    (\(x : G.1.1) -> <i> quotient ((hasIdGroup G).2 x @ i))
    (\(x : factor G P) -> factorIsSet G P (opFactor G P x (idFactor G P)) x)

isAssocFactor (G : group) (P : normalSubgroupProp G) :
  (x y z : factor G P) -> Path (factor G P) (opFactor G P x (opFactor G P y z))
                                            (opFactor G P (opFactor G P x y) z)
  = setQuotIndProp G.1.1 (factorProp G P) C
    (\(x : G.1.1) ->
      setQuotIndProp G.1.1 (factorProp G P) (B (quotient x))
        (\(y : G.1.1) ->
          setQuotIndProp G.1.1 (factorProp G P) (A (quotient x) (quotient y))
            (\(z : G.1.1) -> <i> quotient (isAssocGroup G x y z @ i))
            (propA (quotient x) (quotient y)))
        (propB (quotient x)))
    propC
  where
    op (x y : factor G P) : factor G P = opFactor G P x y
    A (x y z : factor G P) : U
      = Path (factor G P) (op x (op y z)) (op (op x y) z)
    B (x y : factor G P) : U = (z : factor G P) -> A x y z
    C (x : factor G P) : U = (y z : factor G P) -> A x y z
    propA (x y z : factor G P) : isProp (A x y z)
      = setQuotIsSet G.1.1 (factorProp G P) (op x (op y z)) (op (op x y) z)
    propB (x y : factor G P) : isProp (B x y)
      = propPi (factor G P) (A x y) (propA x y)
    propC (x : factor G P) : isProp (C x)
      = propPi (factor G P) (B x) (propB x)

invFactor (G : group) (P : normalSubgroupProp G) : factor G P -> factor G P
  = setQuotLift G.1.1 (factor G P) (factorProp G P) (factorIsSet G P)
    (\(x : G.1.1) -> quotient (invGroup G x))
    (\(x y : G.1.1) (r : P.1.1 (rdiv G x y)) ->
      setQuotId G.1.1 (factorProp G P) (invGroup G x) (invGroup G y)
        (transport (<i> P.1.1 (opGroup G (invGroup G x) (invInvGroup G y @ -i)))
          (normalSubgroupLem G P x y r)))

hasLeftInverseFactor (G : group) (P : normalSubgroupProp G) :
  (x : factor G P) -> Path (factor G P) (opFactor G P (invFactor G P x) x) (idFactor G P)
  = setQuotIndProp G.1.1 (factorProp G P)
    (\(x : factor G P) -> Path (factor G P) (opFactor G P (invFactor G P x) x) (idFactor G P))
    (\(x : G.1.1) -> <i> quotient ((hasInvGroup G).1 x @ i))
    (\(x : factor G P) -> factorIsSet G P (opFactor G P (invFactor G P x) x) (idFactor G P))

hasRightInverseFactor (G : group) (P : normalSubgroupProp G) :
  (x : factor G P) -> Path (factor G P) (opFactor G P x (invFactor G P x)) (idFactor G P)
  = setQuotIndProp G.1.1 (factorProp G P)
    (\(x : factor G P) -> Path (factor G P) (opFactor G P x (invFactor G P x)) (idFactor G P))
    (\(x : G.1.1) -> <i> quotient ((hasInvGroup G).2 x @ i))
    (\(x : factor G P) -> factorIsSet G P (opFactor G P x (invFactor G P x)) (idFactor G P))

factorGroup (G : group) (P : normalSubgroupProp G) : group
  = ((factor G P, factorIsSet G P),
     ((opFactor G P, isAssocFactor G P, idFactor G P,
      (hasLeftIdFactor G P, hasRightIdFactor G P)), invFactor G P,
      (hasLeftInverseFactor G P, hasRightInverseFactor G P)))

subgroupHomo (G : group) (P : subgroupProp G) : grouphom (subgroup G P) G
  = (\(u : (x : G.1.1) * P.1 x) -> u.1,
     (\(u v : (x : G.1.1) * P.1 x) -> <_> opGroup G u.1 v.1, <_> idGroup G))

subgroupSubgroup (G : group) (P Q : subgroupProp G) : subgroupProp (subgroup G Q)
  = (prop, level, ident, inv, op) where
    T : U = subEl G Q
    Q' : group = subgroup G Q
    prop (u : T): U = P.1 u.1
    ident : prop (idGroup Q') = subgroupId G P
    level (x : T) : isProp (prop x) = subgroupLevel G P x.1
    inv (x : T) (p : prop x) : prop (invGroup Q' x) = subgroupInv G P x.1 p
    op (g1 g2 : T) (p : prop g1) (q : prop g2) : prop (opGroup Q' g1 g2) = subgroupOp G P g1.1 g2.1 p q

abelianSubgroupIsNormal (a : abgroup) (P : subgroupProp (abgroup' a))
  : normalSubgroupProp (abgroup' a)
  = (P, (abgroup' a, \(g1 g2 : a.1.1) (p : P.1 g2) -> transport (<i> P.1 (lem2 g1 g2 @ i)) p))
  where
    op (x y : a.1.1) : a.1.1 = opCGroup a x y
    inv (x : a.1.1) : a.1.1 = invCGroup a x
    e : a.1.1 = idCGroup a
    lem1 (g1 g2 : a.1.1) : Path a.1.1 (op g2 (op g1 (inv g1))) g2
      = composition a.1.1 (op g2 (op g1 (inv g1))) (op g2 e) g2
        (<i> op g2 ((hasInvCGroup a).2 g1 @ i))
        ((hasIdCGroup a).2 g2)
    lem2 (g1 g2 : a.1.1) : Path a.1.1 g2 (conjugate (abgroup' a) g1 g2)
      = <i> comp (<_> a.1.1) (isAssocCGroup a g2 g1 (inv g1) @ i)
                            [ (i = 0) -> lem1 g1 g2
                            , (i = 1) -> <j> op (isCommCGroup a g2 g1 @ j) (inv g1) ]

abelianSubgroupIsAbelian (a : abgroup) (P : subgroupProp (abgroup' a)) : abgroup
  = (H.1, (H.2, \(x y : H.1.1) ->
      <i> (isCommCGroup a x.1 y.1 @ i,
           lemPropF G.1.1 P.1 (subgroupLevel G P)
             (opGroup G x.1 y.1) (opGroup G y.1 x.1)
             (isCommCGroup a x.1 y.1)
             (opGroup H x y).2 (opGroup H y x).2 @ i)))
  where
    G : group = abgroup' a
    H : group = subgroup (abgroup' a) P

--- http://cj-xu.github.io/talks/xu-m4c.pdf

isPSh (G: U) (M: monoid): U
  = (c: G -> M.1.1 -> G)
  * (left: (g: G) -> Path G (c g M.2.2.2.1) g)
  * ((g: G) (t r: M.1.1) -> Path G (c (c g t) r) (c g (M.2.1 t r)))

PSh (M: monoid): U
  = (G: U)
  * (isPSh G M)

NatPSh (M: monoid) (D G: PSh M): U
  = (sigma: D.1 -> G.1)
  * ((s: D.1)(t: M.1.1) -> Path G.1 (G.2.1 (sigma s) t) (sigma (D.2.1 s t)))

isType (M: monoid) (G: PSh M) (A: G.1 -> U): U
  = (star: (g: G.1) -> A g -> (t: M.1.1) -> A (G.2.1 g t))
  * (coe1: (g: G.1) (t: M.1.1)   -> Path U (A g) (A (G.2.1 g t)))
  * (coe2: (g: G.1) (t r: M.1.1) -> Path U (A(G.2.1(G.2.1 g t)r))(A(G.2.1 g(M.2.1 t r))))
  * (left: (g: G.1) (a: A g)     -> PathP (coe1 g M.2.2.2.1) a (star g a M.2.2.2.1))
  * ((g:G.1)(a:A g) (t r: M.1.1) -> PathP (coe2 g t r) (star (G.2.1 g t) (star g a t) r)
                                                       (star g a (M.2.1 t r)))

Ctx: monoid -> U = PSh
Substitution: (M: monoid) -> Ctx M -> Ctx M -> U = NatPSh

Type (M: monoid) (G: PSh M): U
  = (A: G.1 -> U)
  * isType M G A

-- A coverage JJ on a monoid M is a collection of subsets of M,
-- called the covering families, satisfying the coverage axiom:
-- for any I∈J and t∈M,there exists a J∈JJ such that for each
-- j∈J there are i∈I and r∈M such that t◦j=i◦r.

-- A presheaf Γ is a sheaf on (M, JJ) if it satisfies the
-- sheaf condition: for any I∈J and any compatible family
-- of elements {γ_i∈Γ|i∈I} there exists a unique amalgamation γ∈Γ
-- such that γ·i = γ_i for all i∈I. -}

-- We need to add a (dependent) sheaf condition to the
-- definition of types in the CwF of sheaves.
-- When verifying the sheaf condition of the universe,
-- we can only show that the amalgamation of a family
-- of elements in Type(M) is unique up to (pointwise) isomorphism.

isDifferentialGroup (G: SET): U
  = (g: isGroup G)
  * (comm: isCommutative G.1 g.1.1)
  * (boundary: G.1 -> G.1)
  * ((x: G.1) -> Path G.1 (boundary (boundary x)) g.1.2.2.1)

unitDGroup: dgroup
  = ((unit,setUnit),(((op,asso,id,(lx,rx)),inv,(li,ri)),comm,b,z)) where
    op: unit -> unit -> unit = \(x y: unit) -> y
    id: unit = tt
    inv: unit -> unit = \(x: unit) -> tt
    lx: (x: unit) -> Path unit (op id x) x = \(x: unit) -> <i> (op id x)
    rx: (x: unit) -> Path unit (op x id) x = split tt -> <i> tt
    li: (x: unit) -> Path unit (op (inv x) x) id = split tt -> <i> tt
    ri: (x: unit) -> Path unit (op x (inv x)) id = split tt -> <i> tt
    b: unit -> unit = idfun unit
    z: (x: unit) -> Path unit (b (b x)) id = split tt -> <i> tt
    asso: isAssociative unit op = \(x y z: unit) -> <i> z
    comm: isCommutative unit op = split tt -> \(y: unit) -> <i> rx y @ -i

-- Group Homomorphism Kernels and Cokernels
-- are just Homotopy Pullbacks and Pushouts pullback.ctt
-- not used, just as simplified definitions

isGroupHom (G H: group) (f: G.1.1 -> H.1.1): U
  = (g1 g2: G.1.1) -> Path H.1.1 (f ((opGroup G) g1 g2)) ((opGroup H) (f g1) (f g2))

isHom (G H: dgroup) (f: G.1.1 -> H.1.1): U
  = isGroupHom (G.1,G.2.1) (H.1,H.2.1) f

isKer (G H: dgroup) (f: G.1.1 -> H.1.1): U
  = (g: G.1.1) -> Path H.1.1 (f g) (idGroup (H.1,H.2.1))

isIm (G H: group) (f: G.1.1 -> H.1.1): U
  = (h: H.1.1) (g: G.1.1) -> Path H.1.1 (f g) h

isKerRing (G H: ring) (f: G.1.1 -> H.1.1): U
  = (g: G.1.1) -> Path H.1.1 (f g) H.2.2.1.1.1.2.2.1

isKerAb (G H: abgroup) (f: G.1.1 -> H.1.1): U
  = (g: G.1.1) -> Path H.1.1 (f g) H.2.1.1.2.2.1