This folder contains a lot of examples implemented using
cubicaltt. The files contain:
+* **algstruct.ctt** - Defines some standard algebraic structures and
+ properties.
+
* **binnat.ctt** - Binary natural numbers and isomorphism to unary
numbers. Example of data and program refinement by
doing a proof for unary numbers by computation with
* **equiv.ctt** - Definition of equivalences and various results on
these, including the "graduate lemma".
+* **grothendieck.ctt** - This file contains a constuction of the Grothendieck
+ group and a proof of its universal property.
+
* **groupoidTrunc.ctt** - The groupoid truncation as a HIT.
* **hedberg.ctt** - Hedberg's lemma: a type with decidable equality is
* **torus.ctt** - Proof that Torus = S1 * S1.
* **univalence.ctt** - Proofs of the univalence axiom.
+
+* **univprop.ctt** - Defines natural transformations, universal arrows, and
+ adjunctions. Also contains a proof that a family of
+ universal arrows gives rise to an adjunction. This is
+ then used to prove that the Grothendieck homomorphism is
+ left adjoint to the forgetful functor.
--- /dev/null
+-- This file contains the definitions of some standard algebraic structures
+-- and homomorphisms, as well as some related identities.
+module algstruct where
+
+import prelude
+import pi
+import sigma
+
+-- Properties
+--------------------------------------------------------------------------------
+
+-- Associativity
+
+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 : set M) (op : M -> M -> M)
+ : prop (isAssociative M op)
+ = let
+ B (a b c : M) : U
+ = Path M (op a (op b c)) (op (op a b) c)
+ h (a b c : M) : prop (B a b c)
+ = sM (op a (op b c)) (op (op a b) c)
+ in propPi3 M B h
+
+-- Has identity element
+
+hasLeftIdentity (M : U) (op : M -> M -> M) (id : M) : U
+ = (x : M) -> Path M (op id x) x
+
+prophasLeftIdentity (M : U) (sM : set M) (op : M -> M -> M) (id : M)
+ : prop (hasLeftIdentity M op id)
+ = let
+ B (x : M) : U
+ = Path M (op id x) x
+ h (x : M) : prop (B x)
+ = sM (op id x) x
+ in propPi M B h
+
+hasRightIdentity (M : U) (op : M -> M -> M) (id : M) : U
+ = (x : M) -> Path M (op x id) x
+
+prophasRightIdentity (M : U) (sM : set M) (op : M -> M -> M) (id : M)
+ : prop (hasRightIdentity M op id)
+ = let
+ B (x : M) : U
+ = Path M (op x id) x
+ h (x : M) : prop (B x)
+ = sM (op x id) x
+ in propPi M B h
+
+hasIdentity (M : U) (op : M -> M -> M) (id : M) : U
+ = (_ : hasLeftIdentity M op id)
+ * (hasRightIdentity M op id)
+
+prophasIdentity (M : U) (sM : set M) (op : M -> M -> M) (id : M)
+ : prop (hasIdentity M op id)
+ = propAnd (hasLeftIdentity M op id) (hasRightIdentity M op id)
+ (prophasLeftIdentity M sM op id) (prophasRightIdentity M sM op id)
+
+-- Commutativity
+
+isCommutative (M : U) (op : M -> M -> M) : U
+ = (x y : M) -> Path M (op x y) (op y x)
+
+propisCommutative (M : U) (sM : set M) (op : M -> M -> M)
+ : prop (isCommutative M op)
+ = let
+ B (x y : M) : U
+ = Path M (op x y) (op y x)
+ h (x y : M) : prop (B x y)
+ = sM (op x y) (op y x)
+ in propPi2 M B h
+
+-- Cancellativity
+
+isLeftCancellative (M : U) (op : M -> M -> M) : U
+ = (c x y : M) -> Path M (op c x) (op c y) -> Path M x y
+
+propisLeftCancellative (M : U) (sM : set M) (op : M -> M -> M)
+ : prop (isLeftCancellative M op)
+ = let
+ B (c x y : M) : U
+ = Path M (op c x) (op c y) -> Path M x y
+ h (c x y : M) : prop (B c x y)
+ = let
+ B0 (p : Path M (op c x) (op c y)) : U
+ = Path M x y
+ h0 (p : Path M (op c x) (op c y)) : prop (B0 p)
+ = sM x y
+ in propPi (Path M (op c x) (op c y)) B0 h0
+ in propPi3 M B h
+
+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 : set M) (op : M -> M -> M)
+ : prop (isRightCancellative M op)
+ = let
+ B (c x y : M) : U
+ = Path M (op x c) (op y c) -> Path M x y
+ h (c x y : M) : prop (B c x y)
+ = let
+ B0 (p : Path M (op x c) (op y c)) : U
+ = Path M x y
+ h0 (p : Path M (op x c) (op y c)) : prop (B0 p)
+ = sM x y
+ in propPi (Path M (op x c) (op y c)) B0 h0
+ in propPi3 M B h
+
+isCancellative (M : U) (op : M -> M -> M) : U
+ = (_ : isLeftCancellative M op)
+ * (isRightCancellative M op)
+
+propisCancellative (M : U) (sM : set M) (op : M -> M -> M)
+ : prop (isCancellative M op)
+ = propAnd (isLeftCancellative M op) (isRightCancellative M op)
+ (propisLeftCancellative M sM op) (propisRightCancellative M sM op)
+
+-- Has inverse element
+
+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 : set G) (op : G -> G -> G) (id : G) (inv : G -> G)
+ : prop (hasLeftInverse G op id inv)
+ = let
+ B (x : G) : U
+ = Path G (op (inv x) x) id
+ h (x : G) : prop (B x)
+ = sG (op (inv x) x) id
+ in propPi G B h
+
+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 : set G) (op : G -> G -> G) (id : G) (inv : G -> G)
+ : prop (hasRightInverse G op id inv)
+ = let
+ B (x : G) : U
+ = Path G (op x (inv x)) id
+ h (x : G) : prop (B x)
+ = sG (op x (inv x)) id
+ in propPi G B h
+
+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 : set G) (op : G -> G -> G) (id : G) (inv : G -> G)
+ : prop (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)
+
+-- Distributivity
+
+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 : set R) (add : R -> R -> R) (mul : R -> R -> R)
+ : prop (isLeftDistributive R add mul)
+ = let
+ 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) : prop (B a b c)
+ = sR (mul a (add b c)) (add (mul a b) (mul a c))
+ in propPi3 R B h
+
+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 : set R) (add : R -> R -> R) (mul : R -> R -> R)
+ : prop (isRightDistributive R add mul)
+ = let
+ 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) : prop (B a b c)
+ = sR (mul (add b c) a) (add (mul b a) (mul c a))
+ in propPi3 R B h
+
+isDistributive (R : U) (add : R -> R -> R) (mul : R -> R -> R) : U
+ = (_ : isLeftDistributive R add mul)
+ * (isRightDistributive R add mul)
+
+propisDistributive (R : U) (sR : set R) (add : R -> R -> R) (mul : R -> R -> R)
+ : prop (isDistributive R add mul)
+ = propAnd (isLeftDistributive R add mul) (isRightDistributive R add mul)
+ (propisLeftDistributive R sR add mul) (propisRightDistributive R sR add mul)
+
+-- Structure preserving properties of maps
+
+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 : set B) (oA : A -> A -> A) (oB : B -> B -> B)
+ (f : A -> B) : prop (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 : set B) (iA : A) (iB : B) (f : A -> B)
+ : prop (preservesId A B iA iB f)
+ = sB (f iA) iB
+
+
+-- Algebraic structures
+--------------------------------------------------------------------------------
+
+-- Group-like structures
+------------------------
+
+-- Monoid
+
+ismonoid (M : SET) : U
+ = (op : M.1 -> M.1 -> M.1)
+ * (_ : isAssociative M.1 op)
+ * (id : M.1)
+ * (hasIdentity M.1 op id)
+
+monoid : U
+ = (X : SET) * ismonoid X
+
+-- Group
+isgroup (G : SET) : U
+ = (m : ismonoid G)
+ * (inv : G.1 -> G.1)
+ * (hasInverse G.1 m.1 m.2.2.1 inv)
+
+group : U
+ = (X : SET) * isgroup X
+
+-- Commutative group-like structures
+------------------------------------
+
+-- Commutative monoid
+
+iscmonoid (M : SET) : U
+ = (m : ismonoid M)
+ * (isCommutative M.1 m.1)
+
+cmonoid : U
+ = (X : SET) * iscmonoid X
+
+-- Commutative group
+
+iscgroup (G : SET) : U
+ = (g : isgroup G)
+ * (isCommutative G.1 g.1.1)
+
+cgroup : U
+ = (X : SET) * iscgroup X
+
+-- Ring-like structures
+-----------------------
+
+-- Ring
+
+isring (R : SET) : U
+ = (mul : ismonoid R)
+ * (add : iscgroup R)
+ * (isDistributive R.1 add.1.1.1 mul.1)
+
+ring : U
+ = (X : SET) * isring X
+
+-- Commutative ring-like structures
+-----------------------------------
+
+-- Commutative ring
+
+iscring (R : SET) : U
+ = (mul : iscmonoid R)
+ * (add : iscgroup R)
+ * (isDistributive R.1 add.1.1.1 mul.1.1)
+
+cring : U
+ = (X : SET) * iscring X
+
+-- Accessors
+------------
+
+-- Monoids
+
+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 : cgroup) : g.1.1 -> g.1.1 -> g.1.1
+ = g.2.1.1.1
+
+isAssocCGroup (g : cgroup) : isAssociative g.1.1 (opCGroup g)
+ = g.2.1.1.2.1
+
+idCGroup (g : cgroup) : g.1.1
+ = g.2.1.1.2.2.1
+
+hasIdCGroup (g : cgroup) : hasIdentity g.1.1 (opCGroup g) (idCGroup g)
+ = g.2.1.1.2.2.2
+
+isCommCGroup (g : cgroup) : isCommutative g.1.1 (opCGroup g)
+ = g.2.2
+
+invCGroup (g : cgroup) : g.1.1 -> g.1.1
+ = g.2.1.2.1
+
+hasInvCGroup (g : cgroup) : hasInverse g.1.1 (opCGroup g) (idCGroup g) (invCGroup g)
+ = g.2.1.2.2
+
+
+-- Simple algebraic properties of commutative groups
+----------------------------------------------------
+
+-- 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)⁻¹ ≡ a⁻¹ · b⁻¹
+lem_cgroup_inv_dist (g : cgroup) (a b : g.1.1)
+ : Path g.1.1 (opCGroup g (invCGroup g a) (invCGroup g b)) (invCGroup g (opCGroup g a b))
+ = let
+ a' : g.1.1
+ = invCGroup g a
+ b' : g.1.1
+ = invCGroup g b
+ x : g.1.1
+ = opCGroup g a b
+ x' : g.1.1
+ = invCGroup g (opCGroup g a b)
+ p0 : Path g.1.1 (opCGroup g x' a) b'
+ = <i> comp (<_> g.1.1) (opCGroup g ((hasInvCGroup g).1 (opCGroup g a b) @ i) b')
+ [ (i = 1) -> (hasIdCGroup g).1 b'
+ , (i = 0) -> <j> comp (<_> g.1.1) (isAssocCGroup g x' x b' @ -j)
+ [ (j = 0) -> <_> opCGroup g (opCGroup g x' x) b'
+ , (j = 1) -> <k> comp (<_> g.1.1) (opCGroup g x' (isAssocCGroup g a b b' @ -k))
+ [ (k = 0) -> <_> opCGroup g x' (opCGroup g x b')
+ , (k = 1) -> <l> comp (<_> g.1.1) (opCGroup g x' (opCGroup g a ((hasInvCGroup g).2 b @ l)))
+ [ (l = 0) -> <_> opCGroup g x' (opCGroup g a (opCGroup g b b'))
+ , (l = 1) -> <m> opCGroup g x' ((hasIdCGroup g).2 a @ m) ]]]]
+ p1 : Path g.1.1 x' (opCGroup g b' a')
+ = <i> comp (<_> g.1.1) (opCGroup g (p0 @ i) a')
+ [ (i = 1) -> <_> opCGroup g b' a'
+ , (i = 0) -> <j> comp (<_> g.1.1) (isAssocCGroup g x' a a' @ -j)
+ [ (j = 0) -> <_> opCGroup g (opCGroup g x' a) a'
+ , (j = 1) -> <k> comp (<_> g.1.1) (opCGroup g x' ((hasInvCGroup g).2 a @ k))
+ [ (k = 0) -> <_> opCGroup g x' (opCGroup g a a')
+ , (k = 1) -> (hasIdCGroup g).2 x' ]]]
+ in <i> comp (<_> g.1.1) (p1 @ -i)
+ [ (i = 0) -> isCommCGroup g (invCGroup g b) (invCGroup g a)
+ , (i = 1) -> <_> invCGroup g (opCGroup g a b) ]
+
+-- e⁻¹ ≡ e
+lemma_cgroup_inv_id (g : cgroup) : Path g.1.1 (invCGroup g (idCGroup g)) (idCGroup g)
+ = <i> comp (<_> g.1.1) ((hasIdCGroup g).2 (invCGroup g (idCGroup g)) @ -i)
+ [ (i = 0) -> <_> invCGroup g (idCGroup g)
+ , (i = 1) -> (hasInvCGroup g).1 (idCGroup g) ]
+
+
+-- 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) : prop (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)
+
+setmonoidhom (a b : monoid) : set (monoidhom a b)
+ = let
+ setf : set (a.1.1 -> b.1.1)
+ = setPi a.1.1 (\ (_ : a.1.1) -> b.1.1) (\ (_ : a.1.1) -> b.1.2)
+ setm (f : a.1.1 -> b.1.1) : set (ismonoidhom a b f)
+ = propSet (ismonoidhom a b f) (propismonoidhom a b f)
+ in setSig (a.1.1 -> b.1.1) (ismonoidhom a b) setf setm
+
+-- 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)
+
+cgrouphom (a b : cgroup) : U
+ = monoidhom (a.1, a.2.1.1) (b.1, b.2.1.1)
+
+cmoncgrouphom (a : cmonoid) (b : cgroup) : U
+ = monoidhom (a.1, a.2.1) (b.1, b.2.1.1)
+
+-- Homomorphism constructors
+
+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 (a.1, a.2.1) (b.1, b.2.1)
+ = let
+ 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 ]
+ in (f, pO, (lem_group_cancellative b).1 (f (idGroup a)) (f (idGroup a)) (idGroup b) p)
+
+cgrouphom' (a b : cgroup) (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' (a.1, a.2.1) (b.1, b.2.1) f pO
+
+-- g ∘ f
+monoidhomcomp (a b c : monoid)
+ (f : monoidhom a b) (g : monoidhom b c)
+ : monoidhom a c
+ = let
+ 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 ]
+ in (h, pO, pI)
+
+-- 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))
+ = let
+ 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)
+ in lemSig (a.1.1 -> d.1.1) (ismonoidhom a d) (propismonoidhom a d) f0 f1 (<_> f0.1)
+
+-- 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
+ = let
+ h : monoidhom a b
+ = monoidhomcomp a a b (idmonoidhom a) f
+ in lemSig (a.1.1 -> b.1.1) (ismonoidhom a b) (propismonoidhom a b) h f (<_> f.1)
+
+-- 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
+ = let
+ h : monoidhom a b
+ = monoidhomcomp a b b f (idmonoidhom b)
+ in lemSig (a.1.1 -> b.1.1) (ismonoidhom a b) (propismonoidhom a b) h f (<_> f.1)
+
+-- 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))
+ = let
+ 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' ]
+ in <i> comp (<_> h.1.1) (p2 @ i)
+ [ (i = 0) -> (hasIdGroup h).1 (f.1 x')
+ , (i = 1) -> <_> y' ]
+
+
+-- Identities of commuative and associative algebraic structures.
+-----------------------------------------------------------------
+
+AscCom : U
+ = (A : U)
+ * (op : A -> A -> A)
+ * (_ : isAssociative A op)
+ * (isCommutative A op)
+
+swp0 (A : AscCom) (a b c : A.1)
+ : Path A.1 (A.2.1 a (A.2.1 b c)) (A.2.1 b (A.2.1 a c))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (asc a b c @ i)
+ [ (i = 0) -> <_> op a (op b c)
+ , (i = 1) -> <j> comp (<_> A.1) (op (cm a b @ j) c)
+ [ (j = 0) -> <_> op (op a b) c
+ , (j = 1) -> <k> asc b a c @ -k ]]
+
+swp1 (A : AscCom) (a b c : A.1)
+ : Path A.1 (A.2.1 a (A.2.1 b c)) (A.2.1 c (A.2.1 b a))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (op a (cm b c @ i))
+ [ (i = 0) -> <_> op a (op b c)
+ , (i = 1) -> <j> comp (<_> A.1) (swp0 A a c b @ j)
+ [ (j = 0) -> <_> op a (op c b)
+ , (j = 1) -> <k> op c (cm a b @ k) ]]
+
+swp2 (A : AscCom) (a b c : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) c) (A.2.1 (A.2.1 c b) a)
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (cm (op a b) c @ i)
+ [ (i = 0) -> <_> op (op a b) c
+ , (i = 1) -> <j> comp (<_> A.1) (swp0 A c a b @ j)
+ [ (j = 0) -> <_> op c (op a b)
+ , (j = 1) -> cm a (op c b) ]]
+
+swp3 (A : AscCom) (a b c : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) c) (A.2.1 (A.2.1 a c) b)
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (cm (op a b) c @ i)
+ [ (i = 0) -> <_> op (op a b) c
+ , (i = 1) -> <j> comp (<_> A.1) (swp1 A c a b @ j)
+ [ (j = 0) -> <_> op c (op a b)
+ , (j = 1) -> cm b (op a c) ]]
+
+swp4 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 a (A.2.1 b (A.2.1 c d))) (A.2.1 c (A.2.1 b (A.2.1 a d)))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (swp0 A a b (op c d) @ i)
+ [ (i = 0) -> <_> op a (op b (op c d))
+ , (i = 1) -> <j> comp (<_> A.1) (op b (swp0 A a c d @ j))
+ [ (j = 0) -> <_> (op b (op a (op c d)))
+ , (j = 1) -> swp0 A b c (op a d) ]]
+
+swp5 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 a (A.2.1 b (A.2.1 c d))) (A.2.1 d (A.2.1 b (A.2.1 c a)))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (swp0 A a b (op c d) @ i)
+ [ (i = 0) -> <_> op a (op b (op c d))
+ , (i = 1) -> <j> comp (<_> A.1) (op b (swp1 A a c d @ j))
+ [ (j = 0) -> <_> (op b (op a (op c d)))
+ , (j = 1) -> swp0 A b d (op c a) ]]
+
+swp6 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) (A.2.1 c d)) (A.2.1 (A.2.1 c b) (A.2.1 a d))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (asc a b (op c d) @ -i)
+ [ (i = 0) -> <_> op (op a b) (op c d)
+ , (i = 1) -> <j> comp (<_> A.1) (swp4 A a b c d @ j)
+ [ (j = 0) -> <_> (op a (op b (op c d)))
+ , (j = 1) -> asc c b (op a d) ]]
+
+swp7 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) (A.2.1 c d)) (A.2.1 (A.2.1 d b) (A.2.1 c a))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (asc a b (op c d) @ -i)
+ [ (i = 0) -> <_> op (op a b) (op c d)
+ , (i = 1) -> <j> comp (<_> A.1) (swp5 A a b c d @ j)
+ [ (j = 0) -> <_> (op a (op b (op c d)))
+ , (j = 1) -> asc d b (op c a) ]]
+
+swp8 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) (A.2.1 c d)) (A.2.1 (A.2.1 a c) (A.2.1 b d))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (asc a b (op c d) @ -i)
+ [ (i = 0) -> <_> op (op a b) (op c d)
+ , (i = 1) -> <j> comp (<_> A.1) (op a (swp0 A b c d @ j))
+ [ (j = 0) -> <_> (op a (op b (op c d)))
+ , (j = 1) -> asc a c (op b d) ]]
+
+swp9 (A : AscCom) (a b c d : A.1)
+ : Path A.1 (A.2.1 (A.2.1 a b) (A.2.1 c d)) (A.2.1 (A.2.1 a d) (A.2.1 c b))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ in <i> comp (<_> A.1) (asc a b (op c d) @ -i)
+ [ (i = 0) -> <_> op (op a b) (op c d)
+ , (i = 1) -> <j> comp (<_> A.1) (op a (swp1 A b c d @ j))
+ [ (j = 0) -> <_> (op a (op b (op c d)))
+ , (j = 1) -> asc a d (op c b) ]]
+
+swptrans (A : AscCom) (k l : A.1) (a b c : and A.1 A.1)
+ (p0 : Path A.1 (A.2.1 k (A.2.1 a.1 b.2)) (A.2.1 k (A.2.1 b.1 a.2)))
+ (p1 : Path A.1 (A.2.1 l (A.2.1 b.1 c.2)) (A.2.1 l (A.2.1 c.1 b.2)))
+ : Path A.1 (A.2.1 (A.2.1 k (A.2.1 l b.2)) (A.2.1 a.1 c.2))
+ (A.2.1 (A.2.1 k (A.2.1 l b.2)) (A.2.1 c.1 a.2))
+ = let
+ op : A.1 -> A.1 -> A.1
+ = A.2.1
+ op3 (x y z : A.1) : A.1
+ = op x (op y z)
+ asc (x y z : A.1) : Path A.1 (op x (op y z)) (op (op x y) z)
+ = A.2.2.1 x y z
+ cm (x y : A.1) : Path A.1 (op x y) (op y x)
+ = A.2.2.2 x y
+ p2 : Path A.1 (op (op l c.2) (op3 k a.1 b.2)) (op (op3 k l b.2) (op a.1 c.2))
+ = <i> comp (<_> A.1) (swp9 A l c.2 a.1 (op k b.2) @ i)
+ [ (i = 0) -> <j> op (op l c.2) (swp0 A k a.1 b.2 @ -j)
+ , (i = 1) -> <j> op (swp0 A l k b.2 @ j) (op a.1 c.2) ]
+ p3 : Path A.1 (op (op l c.2) (op3 k a.1 b.2)) (op (op k a.2) (op3 l b.1 c.2))
+ = <i> comp (<_> A.1) (swp1 A (op l c.2) k (op b.1 a.2) @ i)
+ [ (i = 0) -> <j> op (op l c.2) (p0 @ -j)
+ , (i = 1) -> <j> comp (<_> A.1) (swp6 A b.1 a.2 k (op l c.2) @ j)
+ [ (j = 0) -> <_> op (op b.1 a.2) (op3 k l c.2)
+ , (j = 1) -> <m> op (op k a.2) (swp0 A b.1 l c.2 @ m) ]]
+ p4 : Path A.1 (op (op k a.2) (op3 l b.1 c.2)) (op (op3 k l b.2) (op c.1 a.2))
+ = <i> comp (<_> A.1) (op (op k a.2) (swp0 A l c.1 b.2 @ i))
+ [ (i = 0) -> <j> op (op k a.2) (p1 @ -j)
+ , (i = 1) -> swp9 A k a.2 c.1 (op l b.2) ]
+ in <i> comp (<_> A.1) (p3 @ i) [ (i = 0) -> p2, (i = 1) -> p4 ]
+
+
+
--- /dev/null
+-- This file defines the Grothendieck group of a commutative monoid and proves its
+-- universal property.
+
+module grothendieck where
+
+import setquot
+import algstruct
+
+-- Make setquots abstract
+
+opaque setquot
+opaque setquotpr
+opaque setquotl0
+opaque setquotunivprop
+opaque setquotuniv2prop
+opaque setquotuniv3prop
+opaque setsetquot
+opaque iscompsetquotpr
+opaque setquotmap
+opaque setquotmap2
+opaque setquotmapeq
+opaque setquotmapeq2
+
+
+-- (Mere) existance and shorthand for some related properties
+
+exists (A : U) (B : A -> U) : hProp
+ = ishinh ((x : A) * B x)
+
+existspr (A : U) (B : A -> U) (a : A) (b : B a) : (exists A B).1
+ = hinhpr ((x : A) * B x) (a, b)
+
+existsel (A : U) (B : A -> U) (P : hProp) (f : (x : A) -> (B x) -> P.1) (e : (exists A B).1) : P.1
+ = hinhuniv ((x : A) * B x) P (\(z : (x : A) * (B x)) -> f z.1 z.2) e
+
+existsel2 (A : U) (B : A -> U) (C : U) (D : C -> U) (P : hProp) (f : (x : A) (_ : B x) (y : C) (_ : D y) -> P.1)
+ (e0 : (exists A B).1) (e1 : (exists C D).1) : P.1
+ = let
+ T0 : U
+ = (c : C) (d : D c) -> P.1
+ pT0 : prop T0
+ = propPi C (\(c : C) -> (D c) -> P.1)
+ (\(c : C) -> propPi (D c) (\(_ : D c) -> P.1) (\(_ : D c) -> P.2))
+ in existsel C D P (existsel A B (T0, pT0) f e0) e1
+
+
+-- Shorthand for commuative monoids and groups
+
+op (m : cmonoid) : m.1.1 -> m.1.1 -> m.1.1
+ = opCMonoid m
+
+op3 (m : cmonoid) : m.1.1 -> m.1.1 -> m.1.1 -> m.1.1
+ = \ (a b c : m.1.1) -> op m a (op m b c)
+
+asc (m : cmonoid) : isAssociative m.1.1 (op m)
+ = isAssocCMonoid m
+
+id (m : cmonoid) : m.1.1
+ = idCMonoid m
+
+hid (m : cmonoid) : hasIdentity m.1.1 (op m) (id m)
+ = hasIdCMonoid m
+
+cm (m : cmonoid) : isCommutative m.1.1 (op m)
+ = isCommCMonoid m
+
+ac (m : cmonoid) : AscCom
+ = (m.1.1, op m, asc m, cm m)
+
+gac (g : cgroup) : AscCom
+ = (g.1.1, opCGroup g, isAssocCGroup g, isCommCGroup g)
+
+
+-- Direct product of a cancellative monoid with appropriate operators and properties
+
+pair (m : cmonoid) : U
+ = and m.1.1 m.1.1
+
+pset (m : cmonoid) : set (pair m)
+ = setSig m.1.1 (\(_ : m.1.1) -> m.1.1) m.1.2 (\(_ : m.1.1) -> m.1.2)
+
+pop (m : cmonoid) (x y : pair m) : pair m
+ = (op m x.1 y.1, op m x.2 y.2)
+
+pid (m : cmonoid) : pair m
+ = (id m, id m)
+
+phid (m : cmonoid) : hasIdentity (pair m) (pop m) (pid m)
+ = ( \ (x : pair m) -> <i> ((hid m).1 x.1 @ i, (hid m).1 x.2 @ i)
+ , \ (x : pair m) -> <i> ((hid m).2 x.1 @ i, (hid m).2 x.2 @ i) )
+
+pasc (m : cmonoid) : isAssociative (pair m) (pop m)
+ = \ (x0 x1 x2 : pair m) -> <i> (asc m x0.1 x1.1 x2.1 @ i, asc m x0.2 x1.2 x2.2 @ i)
+
+pcm (m : cmonoid) : isCommutative (pair m) (pop m)
+ = \ (x0 x1 : pair m) -> <i> (cm m x0.1 x1.1 @ i, cm m x0.2 x1.2 @ i)
+
+
+-- Equivalence relation on pair
+
+prel (m : cmonoid) (a b : pair m) : hProp
+ = let
+ T (t : m.1.1) : U
+ = Path m.1.1 (op3 m t a.1 b.2) (op3 m t b.1 a.2)
+ in exists m.1.1 T
+
+prelisrefl (m : cmonoid) (a : pair m) : (prel m a a).1 -- exists m.1.1 T pT
+ = let
+ T (k : m.1.1) : U
+ = Path m.1.1 (op3 m k a.1 a.2) (op3 m k a.1 a.2)
+ k : m.1.1
+ = id m
+ in existspr m.1.1 T k (<i> op m (id m) (op m a.1 a.2))
+
+prelissymm (m : cmonoid) (a b : pair m) (p0 : (prel m a b).1) : (prel m b a).1
+ = let
+ T0 (t : m.1.1) : U
+ = Path m.1.1 (op3 m t a.1 b.2) (op3 m t b.1 a.2)
+ T1 (t : m.1.1) : U
+ = Path m.1.1 (op3 m t b.1 a.2) (op3 m t a.1 b.2)
+ f (k : m.1.1) (p : T0 k) : (exists m.1.1 T1).1
+ = existspr m.1.1 T1 k (<i> p @ -i)
+ P : hProp
+ = exists m.1.1 T1
+ in existsel m.1.1 T0 (exists m.1.1 T1) f p0
+
+prelistrans (m : cmonoid) (x y z : pair m) (p0 : (prel m x y).1) (p1 : (prel m y z).1)
+ : (prel m x z).1
+ = let
+ T0 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.1 y.2) (op3 m k y.1 x.2)
+ T1 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k y.1 z.2) (op3 m k z.1 y.2)
+ T2 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.1 z.2) (op3 m k z.1 x.2)
+ f (k : m.1.1) (p0 : T0 k) (l : m.1.1) (p1 : T1 l) : (exists m.1.1 T2).1
+ = existspr m.1.1 T2 (op m k (op m l y.2))
+ (swptrans (ac m) k l (x.1, x.2) (y.1, y.2) (z.1, z.2) p0 p1)
+ in existsel2 m.1.1 T0 m.1.1 T1 (exists m.1.1 T2) f p0 p1
+
+peqrel (m : cmonoid) : eqrel (pair m)
+ = (prel m, ((prelistrans m, prelisrefl m), prelissymm m))
+
+
+-- The Grothendieck group of a commutative monoid M is constructed by taking
+-- the quotient pair(M) / prel(M)
+
+qgroup (m : cmonoid) : U
+ = setquot (pair m) (prel m)
+
+qpr (m : cmonoid) (x : pair m) : qgroup m
+ = setquotpr (pair m) (peqrel m) x
+
+setqgroup (m : cmonoid) : set (qgroup m)
+ = setsetquot (pair m) (prel m)
+
+opaque setqgroup
+
+
+-- Group structure of the Grothendieck group
+
+qid (m : cmonoid) : qgroup m
+ = qpr m (pid m)
+
+qop' (m : cmonoid) (x0 x1 : pair m) : qgroup m
+ = qpr m (pop m x0 x1)
+
+qop'resprel (m : cmonoid) (x x' y y' : pair m) (p0 : (prel m x x').1)
+ (p1 : (prel m y y').1) : Path (qgroup m) (qop' m x y) (qop' m x' y')
+ = let
+ z0 : pair m
+ = pop m x y
+ z1 : pair m
+ = pop m x' y'
+ T0 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.1 x'.2) (op3 m k x'.1 x.2)
+ T1 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k y.1 y'.2) (op3 m k y'.1 y.2)
+ T2 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k z0.1 z1.2) (op3 m k z1.1 z0.2)
+ T3 : U
+ = Path (qgroup m) (qop' m x y) (qop' m x' y')
+ pT3 : prop T3
+ = setqgroup m (qop' m x y) (qop' m x' y')
+ f (k : m.1.1) (p0 : T0 k) (l : m.1.1) (p1 : T1 l) : T3
+ = let
+ n : m.1.1
+ = op m k l
+ p : Path m.1.1 (op3 m n z0.1 z1.2) (op3 m n z1.1 z0.2)
+ = <i> comp (<_> m.1.1) (op m (p0 @ i) (p1 @ i))
+ [ (i = 0) -> <j> comp (<_> m.1.1) (swp8 (ac m) k (op m x.1 x'.2) l (op m y.1 y'.2) @ j)
+ [ (j = 0) -> <_> (op m (op3 m k x.1 x'.2) (op3 m l y.1 y'.2))
+ , (j = 1) -> <h> op m (op m k l) (swp8 (ac m) x.1 x'.2 y.1 y'.2 @ h) ]
+ , (i = 1) -> <j> comp (<_> m.1.1) (swp8 (ac m) k (op m x'.1 x.2) l (op m y'.1 y.2) @ j)
+ [ (j = 0) -> <_> (op m (op3 m k x'.1 x.2) (op3 m l y'.1 y.2))
+ , (j = 1) -> <h> op m (op m k l) (swp8 (ac m) x'.1 x.2 y'.1 y.2 @ h) ]]
+ e : (prel m z0 z1).1
+ = existspr m.1.1 T2 n p
+ in iscompsetquotpr (pair m) (peqrel m) z0 z1 e
+ in existsel2 m.1.1 T0 m.1.1 T1 (T3, pT3) f p0 p1
+
+opaque qop'resprel
+
+qop (m : cmonoid) (q0 q1 : qgroup m) : qgroup m
+ = setquotmap2 (pair m) (pair m) (qgroup m) (setqgroup m) (prel m)
+ (prel m) (qop' m) (qop'resprel m) q0 q1
+
+qopeq (m : cmonoid) (x0 x1 : pair m)
+ : Path (qgroup m) (qop m (qpr m x0) (qpr m x1)) (qop' m x0 x1)
+ = setquotmapeq2 (pair m) (pair m) (qgroup m) (setqgroup m) (peqrel m)
+ (peqrel m) (qop' m) (qop'resprel m) x0 x1
+
+opaque qopeq
+
+qinv' (m : cmonoid) (x0 : pair m) : qgroup m
+ = qpr m (x0.2, x0.1)
+
+qinv'resprel (m : cmonoid) (x y : pair m) (r : (prel m x y).1)
+ : Path (qgroup m) (qinv' m x) (qinv' m y)
+ = let
+ T0 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.1 y.2) (op3 m k y.1 x.2)
+ T1 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.2 y.1) (op3 m k y.2 x.1)
+ f (k : m.1.1) (p : T0 k) : (exists m.1.1 T1).1
+ = existspr m.1.1 T1 k (<i> comp (<_> m.1.1) (p @ -i)
+ [ (i = 0) -> <j> op m k (cm m y.1 x.2 @ j)
+ , (i = 1) -> <j> op m k (cm m x.1 y.2 @ j) ])
+ in iscompsetquotpr (pair m) (peqrel m) (x.2, x.1) (y.2, y.1)
+ (existsel m.1.1 T0 (exists m.1.1 T1) f r)
+
+opaque qinv'resprel
+
+qinv (m : cmonoid) (q : qgroup m) : qgroup m
+ = setquotmap (pair m) (qgroup m) (setqgroup m) (prel m) (qinv' m)
+ (qinv'resprel m) q
+
+qinveq (m : cmonoid) (x : pair m) : Path (qgroup m) (qinv m (qpr m x)) (qinv' m x)
+ = setquotmapeq (pair m) (qgroup m) (setqgroup m) (peqrel m)
+ (qinv' m) (qinv'resprel m) x
+
+opaque qinveq
+
+qhli (m : cmonoid) : hasLeftInverse (qgroup m) (qop m) (qid m) (qinv m)
+ = \ (q : qgroup m) -> let
+ tP (x : qgroup m) : U
+ = Path (qgroup m) (qop m (qinv m x) x) (qid m)
+ ps (x : pair m) : tP (qpr m x)
+ = let
+ T (k : m.1.1) : U
+ = Path m.1.1 (op m k (op m (op m x.2 x.1) (id m)))
+ (op m k (op m (id m) (op m x.1 x.2)))
+ p0 : Path (qgroup m) (qop m (qinv m (qpr m x)) (qpr m x)) (qop' m (x.2, x.1) x)
+ = <i> comp (<_> qgroup m) (qop m (qinveq m x @ i) (qpr m x))
+ [ (i = 0) -> <_> qop m (qinv m (qpr m x)) (qpr m x)
+ , (i = 1) -> qopeq m (x.2, x.1) x ]
+ p1 : Path m.1.1 (op m (id m) (op m (op m x.2 x.1) (id m)))
+ (op m (id m) (op m (id m) (op m x.1 x.2)))
+ = <i> op m (id m) (comp (<j> m.1.1) (cm m (op m x.2 x.1) (id m) @ i)
+ [ (i = 0) -> <j> (op m (op m x.2 x.1) (id m))
+ , (i = 1) -> <j> op m (id m) (cm m x.2 x.1 @ j) ])
+ p2 : Path (qgroup m) (qop' m (x.2, x.1) x) (qid m)
+ = iscompsetquotpr (pair m) (peqrel m) (pop m (x.2, x.1) x) (pid m)
+ (existspr m.1.1 T (id m) p1)
+ in <i> comp (<_> qgroup m) (p0 @ i)
+ [ (i = 0) -> <_> p0 @ 0
+ , (i = 1) -> p2 ]
+ pP (x : qgroup m) : prop (tP x)
+ = setqgroup m (qop m (qinv m x) x) (qid m)
+ P (x : qgroup m) : hProp
+ = (tP x, pP x)
+ in setquotunivprop (pair m) (peqrel m) P ps q
+
+qhri (m : cmonoid) : hasRightInverse (qgroup m) (qop m) (qid m) (qinv m)
+ = \ (q : qgroup m) -> let
+ tP (x : qgroup m) : U
+ = Path (qgroup m) (qop m x (qinv m x)) (qid m)
+ ps (x : pair m) : tP (qpr m x)
+ = let
+ T (k : m.1.1) : U
+ = Path m.1.1 (op m k (op m (op m x.1 x.2) (id m)))
+ (op m k (op m (id m) (op m x.2 x.1)))
+ p0 : Path (qgroup m) (qop m (qpr m x) (qinv m (qpr m x))) (qop' m x (x.2, x.1))
+ = <i> comp (<_> qgroup m) (qop m (qpr m x) (qinveq m x @ i))
+ [ (i = 0) -> <_> qop m (qpr m x) (qinv m (qpr m x))
+ , (i = 1) -> qopeq m x (x.2, x.1) ]
+ p1 : Path m.1.1 (op m (id m) (op m (op m x.1 x.2) (id m)))
+ (op m (id m) (op m (id m) (op m x.2 x.1)))
+ = <i> op m (id m) (comp (<j> m.1.1) (cm m (op m x.1 x.2) (id m) @ i)
+ [ (i = 0) -> <j> (op m (op m x.1 x.2) (id m))
+ , (i = 1) -> <j> op m (id m) (cm m x.1 x.2 @ j) ])
+ p2 : Path (qgroup m) (qop' m x (x.2, x.1)) (qid m)
+ = iscompsetquotpr (pair m) (peqrel m) (pop m x (x.2, x.1)) (pid m)
+ (existspr m.1.1 T (id m) p1)
+ in <i> comp (<_> qgroup m) (p0 @ i)
+ [ (i = 0) -> <_> p0 @ 0
+ , (i = 1) -> p2 ]
+ pP (x : qgroup m) : prop (tP x)
+ = setqgroup m (qop m x (qinv m x)) (qid m)
+ P (x : qgroup m) : hProp
+ = (tP x, pP x)
+ in setquotunivprop (pair m) (peqrel m) P ps q
+
+qlid (m : cmonoid) : hasLeftIdentity (qgroup m) (qop m) (qid m)
+ = \ (q : qgroup m) -> let
+ tP (x : qgroup m) : U
+ = Path (qgroup m) (qop m (qid m) x) x
+ ps (x : pair m) : tP (qpr m x)
+ = let
+ p0 : Path (qgroup m) (qop m (qid m) (qpr m x)) (qop' m (pid m) x)
+ = qopeq m (pid m) x
+ p1 : Path (qgroup m) (qop' m (pid m) x) (qpr m x)
+ = <i> qpr m ((phid m).1 x @ i)
+ in <i> comp (<_> qgroup m) (p0 @ i)
+ [ (i = 0) -> <_> p0 @ 0
+ , (i = 1) -> p1 ]
+ pP (x : qgroup m) : prop (tP x)
+ = setqgroup m (qop m (qid m) x) x
+ P (x : qgroup m) : hProp
+ = (tP x, pP x)
+ in setquotunivprop (pair m) (peqrel m) P ps q
+
+qrid (m : cmonoid) : hasRightIdentity (qgroup m) (qop m) (qid m)
+ = \ (q : qgroup m) -> let
+ tP (x : qgroup m) : U
+ = Path (qgroup m) (qop m x (qid m)) x
+ ps (x : pair m) : tP (qpr m x)
+ = let
+ p0 : Path (qgroup m) (qop m (qpr m x) (qid m)) (qop' m x (pid m))
+ = qopeq m x (pid m)
+ p1 : Path (qgroup m) (qop' m x (pid m)) (qpr m x)
+ = <i> qpr m ((phid m).2 x @ i)
+ in <i> comp (<_> qgroup m) (p0 @ i)
+ [ (i = 0) -> <_> p0 @ 0
+ , (i = 1) -> p1 ]
+ pP (x : qgroup m) : prop (tP x)
+ = setqgroup m (qop m x (qid m)) x
+ P (x : qgroup m) : hProp
+ = (tP x, pP x)
+ in setquotunivprop (pair m) (peqrel m) P ps q
+
+qasc (m : cmonoid) : isAssociative (qgroup m) (qop m)
+ = \ (q0 q1 q2 : qgroup m) -> let
+ tP (x0 x1 x2 : qgroup m) : U
+ = Path (qgroup m) (qop m x0 (qop m x1 x2)) (qop m (qop m x0 x1) x2)
+ ps (x0 x1 x2 : pair m) : tP (qpr m x0) (qpr m x1) (qpr m x2)
+ = let
+ p0 : Path (qgroup m) (qop m (qpr m x0) (qop m (qpr m x1) (qpr m x2)))
+ (qpr m (pop m x0 (pop m x1 x2)))
+ = <i> comp (<_> qgroup m) (qop m (qpr m x0) (qopeq m x1 x2 @ i))
+ [ (i = 0) -> <_> qop m (qpr m x0) (qop m (qpr m x1) (qpr m x2))
+ , (i = 1) -> qopeq m x0 (pop m x1 x2) ]
+ p1 : Path (qgroup m) (qpr m (pop m x0 (pop m x1 x2)))
+ (qpr m (pop m (pop m x0 x1) x2))
+ = <i> qpr m (pasc m x0 x1 x2 @ i)
+ p2 : Path (qgroup m) (qop m (qop m (qpr m x0) (qpr m x1)) (qpr m x2))
+ (qpr m (pop m (pop m x0 x1) x2))
+ = <i> comp (<_> qgroup m) (qop m (qopeq m x0 x1 @ i) (qpr m x2))
+ [ (i = 0) -> <_> qop m (qop m (qpr m x0) (qpr m x1)) (qpr m x2)
+ , (i = 1) -> qopeq m (pop m x0 x1) x2 ]
+ in <i> comp (<_> qgroup m) (p1 @ i)
+ [ (i = 0) -> <j> p0 @ -j
+ , (i = 1) -> <j> p2 @ -j ]
+ pP (x0 x1 x2 : qgroup m) : prop (tP x0 x1 x2)
+ = setqgroup m (qop m x0 (qop m x1 x2)) (qop m (qop m x0 x1) x2)
+ P (x0 x1 x2 : qgroup m) : hProp
+ = (tP x0 x1 x2, pP x0 x1 x2)
+ in setquotuniv3prop (pair m) (peqrel m) P ps q0 q1 q2
+
+qc (m : cmonoid) : isCommutative (qgroup m) (qop m)
+ = \ (q0 q1 : qgroup m) -> let
+ tP (x0 x1 : qgroup m) : U
+ = Path (qgroup m) (qop m x0 x1) (qop m x1 x0)
+ ps (x0 x1 : pair m) : tP (qpr m x0) (qpr m x1)
+ = <i> comp (<_> qgroup m) (qpr m (pcm m x0 x1 @ i))
+ [ (i = 0) -> <j> qopeq m x0 x1 @ -j
+ , (i = 1) -> <j> qopeq m x1 x0 @ -j ]
+ pP (x0 x1 : qgroup m) : prop (tP x0 x1)
+ = setqgroup m (qop m x0 x1) (qop m x1 x0)
+ P (x0 x1 : qgroup m) : hProp
+ = (tP x0 x1, pP x0 x1)
+ in setquotuniv2prop (pair m) (peqrel m) P ps q0 q1
+
+-- The Grothendieck group
+
+grothendieck (m : cmonoid) : cgroup
+ = ( (qgroup m, setqgroup m)
+ , (((qop m, qasc m, qid m, (qlid m , qrid m)), qinv m, (qhli m, qhri m))
+ , qc m))
+
+-- The underlying commutative monoid of a commutative group
+forgetfulAb (g : cgroup) : cmonoid
+ = (g.1, (g.2.1.1,g.2.2))
+
+-- The canonical homomorphism π : m → K₀(M)
+grothendieckhom (m : cmonoid) : cmoncgrouphom m (grothendieck m)
+ = let
+ g : cgroup
+ = grothendieck m
+ f (x : m.1.1) : g.1.1
+ = qpr m (x, id m)
+ pop : preservesOp m.1.1 g.1.1 (op m) (g.2.1.1.1) f
+ = \ (a0 a1 : m.1.1) ->
+ <i> comp (<j> g.1.1) (qopeq m (a0, id m) (a1, id m) @ -i)
+ [ (i = 0) -> <j> qpr m (op m a0 a1, (hid m).1 (id m) @ j)
+ , (i = 1) -> <j> (g.2.1.1.1 (f a0) (f a1)) ]
+ pid : preservesId m.1.1 g.1.1 (id m) (g.2.1.1.2.2.1) f
+ = <i> qpr m (id m, id m)
+ in (f, (pop, pid))
+
+-- a · b = c · d ⇒ a · d⁻¹ = c · b⁻¹
+gswp10 (g : cgroup) (a b c d : g.1.1) (p : Path g.1.1 (g.2.1.1.1 a b) (g.2.1.1.1 c d))
+ : Path g.1.1 (g.2.1.1.1 a (g.2.1.2.1 d)) (g.2.1.1.1 c (g.2.1.2.1 b))
+ = let
+ b' : g.1.1
+ = g.2.1.2.1 b
+ d' : g.1.1
+ = g.2.1.2.1 d
+ p0 : Path g.1.1 (g.2.1.1.1 (g.2.1.1.1 a b) (g.2.1.1.1 b' d'))
+ (g.2.1.1.1 (g.2.1.1.1 c d) (g.2.1.1.1 b' d'))
+ = <i> g.2.1.1.1 (p @ i) (g.2.1.1.1 b' d')
+ p1 : Path g.1.1 (g.2.1.1.1 (g.2.1.1.1 a b) (g.2.1.1.1 b' d')) (g.2.1.1.1 a d')
+ = <i> comp (<_> g.1.1) (g.2.1.1.1 (g.2.1.1.1 a d') ((g.2.1.2.2).1 b @ i))
+ [ (i = 0) -> <i> swp9 (gac g) a b b' d' @ -i
+ , (i = 1) -> (g.2.1.1.2.2.2).2 (g.2.1.1.1 a d') ]
+ p2 : Path g.1.1 (g.2.1.1.1 (g.2.1.1.1 c d) (g.2.1.1.1 b' d')) (g.2.1.1.1 c b')
+ = <i> comp (<_> g.1.1) (g.2.1.1.1 (g.2.1.1.1 c b') ((g.2.1.2.2).2 d @ i))
+ [ (i = 0) -> <i> swp8 (gac g) c d b' d' @ -i
+ , (i = 1) -> (g.2.1.1.2.2.2).2 (g.2.1.1.1 c b') ]
+ in <i> comp (<_> g.1.1) (p0 @ i)
+ [ (i = 0) -> p1
+ , (i = 1) -> p2 ]
+
+
+-- The universal property of the Grothendieck group
+
+-- g(x) :≡ f(x.1) · f(x.2)⁻¹
+grothendiecklem0 (m : cmonoid) (a : cgroup) (f : cmoncgrouphom m a)
+ (x : pair m) : a.1.1
+ = a.2.1.1.1 (f.1 x.1) (a.2.1.2.1 (f.1 x.2))
+
+-- x ~ y ⇒ g(x) = g(y)
+grothendiecklem1 (m : cmonoid) (a : cgroup) (f : cmoncgrouphom m a)
+ : funresprel (pair m) a.1.1 (grothendiecklem0 m a f) (prel m)
+ = \ (x y : pair m) (r : (prel m x y).1) -> let
+ g : pair m -> a.1.1
+ = grothendiecklem0 m a f
+ T0 (k : m.1.1) : U
+ = Path m.1.1 (op3 m k x.1 y.2) (op3 m k y.1 x.2)
+ h (k : m.1.1) (p : T0 k)
+ : Path a.1.1 (g x) (g y)
+ = let
+ p0 : Path a.1.1 (a.2.1.1.1 (f.1 k) (f.1 (op m x.1 y.2))) (a.2.1.1.1 (f.1 k) (f.1 (op m y.1 x.2)))
+ = <i> comp (<_> a.1.1) (f.1 (p @ i))
+ [ (i = 0) -> f.2.1 k (op m x.1 y.2)
+ , (i = 1) -> f.2.1 k (op m y.1 x.2) ]
+ p1 : Path a.1.1 (f.1 (op m x.1 y.2)) (f.1 (op m y.1 x.2))
+ = lem_group_lcancellative (a.1, a.2.1) (f.1 k) (f.1 (op m x.1 y.2)) (f.1 (op m y.1 x.2)) p0
+ p2 : Path a.1.1 (a.2.1.1.1 (f.1 x.1) (f.1 y.2)) (a.2.1.1.1 (f.1 y.1) (f.1 x.2))
+ = <i> comp (<_> a.1.1) (p1 @ i)
+ [ (i = 0) -> f.2.1 x.1 y.2
+ , (i = 1) -> f.2.1 y.1 x.2 ]
+ in gswp10 a (f.1 x.1) (f.1 y.2) (f.1 y.1) (f.1 x.2) p2
+ in existsel m.1.1 T0 (Path a.1.1 (g x) (g y), a.1.2 (g x) (g y)) h r
+
+-- h : K₀(m) → a
+grothendiecklem2 (m : cmonoid) (a : cgroup) (f : cmoncgrouphom m a)
+ : (grothendieck m).1.1 -> a.1.1
+ = setquotmap (pair m) a.1.1 a.1.2 (prel m) (grothendiecklem0 m a f) (grothendiecklem1 m a f)
+
+-- h([x]) → g(x)
+grothendiecklem3 (m : cmonoid) (a : cgroup) (f : cmoncgrouphom m a) (x : pair m)
+ : Path a.1.1 (grothendiecklem2 m a f (qpr m x)) (grothendiecklem0 m a f x)
+ = setquotmapeq (pair m) a.1.1 a.1.2 (peqrel m) (grothendiecklem0 m a f) (grothendiecklem1 m a f) x
+
+-- h is a homomorphism
+grothendiecklem4 (m : cmonoid) (a : cgroup)
+ (f : cmoncgrouphom m a) : cgrouphom (grothendieck m) a
+ = let
+ agop (g : cgroup) : g.1.1 -> g.1.1 -> g.1.1
+ = g.2.1.1.1
+ agop3 (g : cgroup) : g.1.1 -> g.1.1 -> g.1.1 -> g.1.1
+ = \ (a b c : g.1.1) -> agop g a (agop g b c)
+ agid (g : cgroup) : g.1.1
+ = g.2.1.1.2.2.1
+ aginv (g : cgroup) : g.1.1 -> g.1.1
+ = g.2.1.2.1
+ k : cgroup
+ = grothendieck m
+ g' : pair m -> a.1.1
+ = grothendiecklem0 m a f
+ g : k.1.1 -> a.1.1
+ = grothendiecklem2 m a f
+ geq (x : pair m) : Path a.1.1 (g (qpr m x)) (g' x)
+ = grothendiecklem3 m a f x
+ pO : preservesOp k.1.1 a.1.1 (agop k) (agop a) g
+ = \(x0 x1 : k.1.1) -> let
+ P (x0 x1 : k.1.1) : hProp
+ = ( Path a.1.1 (g (agop k x0 x1)) (agop a (g x0) (g x1))
+ , a.1.2 (g (agop k x0 x1)) (agop a (g x0) (g x1)) )
+ ps (a0 a1 : pair m) : (P (qpr m a0) (qpr m a1)).1
+ = let
+ x0 : k.1.1
+ = qpr m a0
+ x1 : k.1.1
+ = qpr m a1
+ b0 : m.1.1
+ = op m a0.1 a1.1
+ b1 : m.1.1
+ = op m a0.2 a1.2
+ p : Path a.1.1 (g (agop k x0 x1)) (agop a (f.1 b0) (aginv a (f.1 b1)))
+ = <i> comp (<_> a.1.1) (g (qopeq m a0 a1 @ i))
+ [ (i = 0) -> <_> g (agop k x0 x1)
+ , (i = 1) -> geq (pop m a0 a1) ]
+ q' : Path a.1.1 (agop a (g' a0) (g' a1))
+ (agop a (agop a (f.1 a0.1) (f.1 a1.1))
+ (aginv a (agop a (f.1 a0.2) (f.1 a1.2))))
+ = <i> comp (<_> a.1.1) (swp8 (gac a) (f.1 a0.1)
+ (aginv a (f.1 a0.2)) (f.1 a1.1) (aginv a (f.1 a1.2)) @ i)
+ [ (i = 0) -> <j> (agop a (g' a0) (g' a1))
+ , (i = 1) -> <j> (agop a (agop a (f.1 a0.1) (f.1 a1.1))
+ (lem_cgroup_inv_dist a (f.1 a0.2) (f.1 a1.2) @ j)) ]
+ q : Path a.1.1 (agop a (g x0) (g x1)) (agop a (f.1 b0) (aginv a (f.1 b1)))
+ = <i> comp (<_> a.1.1) (q' @ i)
+ [ (i = 0) -> <j> agop a (geq a0 @ -j) (geq a1 @ -j)
+ , (i = 1) -> <j> agop a (f.2.1 a0.1 a1.1 @ -j) (aginv a (f.2.1 a0.2 a1.2 @ -j)) ]
+ in <i> comp (<_> a.1.1) (p @ i)
+ [ (i = 0) -> <_> g (agop k x0 x1) -- (g (agop k x0 x1))
+ , (i = 1) -> <j> q @ -j ] -- (agop a (f.1 b0) (aginv a (f.1 b1)))
+ in setquotuniv2prop (pair m) (peqrel m) P ps x0 x1
+ in cgrouphom' k a g pO
+
+-- A proof that the following diagram commutes:
+--
+-- π
+-- M --------> K₀(M)
+-- \ |
+-- \ |
+-- ------- | ∃!h
+-- f \ |
+-- \ v
+-- G
+--
+-- meaning that there is a unique h such that f ≡ h ∘ π
+grothendieckunivprop' (m : cmonoid) (a : cgroup) (f : cmoncgrouphom m a)
+ : isContr( (g : cgrouphom (grothendieck m) a)
+ * Path (cmoncgrouphom m a) f (monoidhomcomp (m.1, m.2.1) ((grothendieck m).1, (grothendieck m).2.1.1)
+ (a.1, a.2.1.1) (grothendieckhom m) g))
+ = let
+ aop (a : cgroup) : a.1.1 -> a.1.1 -> a.1.1
+ = a.2.1.1.1
+ aneg (a : cgroup) : a.1.1 -> a.1.1
+ = a.2.1.2.1
+ aid (a : cgroup) : a.1.1
+ = a.2.1.1.2.2.1
+ groth : cgroup
+ = grothendieck m
+ T0 : U
+ = cgrouphom groth a
+ T1 (g : T0) : U
+ = Path (cmoncgrouphom m a) f (monoidhomcomp (m.1, m.2.1) (groth.1, groth.2.1.1) (a.1, a.2.1.1) (grothendieckhom m) g)
+ pT1 (g : T0) : prop (T1 g)
+ = setmonoidhom (m.1, m.2.1) (a.1, a.2.1.1) f (monoidhomcomp (m.1, m.2.1) (groth.1, groth.2.1.1) (a.1, a.2.1.1) (grothendieckhom m) g)
+ T : U
+ = (g : T0) * T1 g
+ g : cgrouphom groth a
+ = grothendiecklem4 m a f
+ p : T1 g
+ = let
+ p0 : Path (m.1.1 -> a.1.1) f.1 (\ (x : m.1.1) -> grothendiecklem2 m a f (qpr m (x, id m)))
+ = <i> \ (x : m.1.1) -> comp (<_> a.1.1) (aop a (f.1 x) (aneg a (aid a)))
+ [ (i = 0) -> <j> comp (<_> a.1.1) (aop a (f.1 x) (aid a))
+ [ (j = 0) -> <k> aop a (f.1 x) (lemma_cgroup_inv_id a @ -k)
+ , (j = 1) -> a.2.1.1.2.2.2.2 (f.1 x) ]
+ , (i = 1) -> <j> comp (<_> a.1.1) (aop a (f.1 x) (aneg a (f.1 (id m))))
+ [ (j = 0) -> <j> aop a (f.1 x) (aneg a (f.2.2 @ j))
+ , (j = 1) -> <k> grothendiecklem3 m a f (x, id m) @ -k ]]
+ in lemSig (m.1.1 -> a.1.1) (ismonoidhom (m.1, m.2.1) (a.1, a.2.1.1)) (propismonoidhom (m.1, m.2.1) (a.1, a.2.1.1)) f
+ (monoidhomcomp (m.1, m.2.1) (groth.1, groth.2.1.1) (a.1, a.2.1.1) (grothendieckhom m) g) p0
+ x : T
+ = (g, p)
+ cntr (y : T) : Path T x y
+ = let
+ GH : U
+ = cgrouphom groth a
+ g' : cgrouphom groth a
+ = y.1
+ p' : Path (cmoncgrouphom m a) f
+ (monoidhomcomp (m.1, m.2.1) (groth.1, groth.2.1.1) (a.1, a.2.1.1) (grothendieckhom m) g')
+ = y.2
+ p0 (x : m.1.1) : Path a.1.1 (g.1 (qpr m (x, id m))) (g'.1 (qpr m (x, id m)))
+ = <i> comp (<_> a.1.1) (f.1 x)
+ [ (i = 0) -> <j> (p @ j).1 x
+ , (i = 1) -> <j> (p' @ j).1 x ]
+ P (x : qgroup m) : hProp
+ = (Path a.1.1 (g.1 x) (g'.1 x), a.1.2 (g.1 x) (g'.1 x))
+ p1 (x : pair m) : Path a.1.1 (g.1 (qpr m x)) (g'.1 (qpr m x))
+ = let
+ p1' (g : GH) : Path a.1.1 (g.1 (qpr m x)) (aop a (g.1 (qpr m (x.1, id m))) (aneg a (g.1 (qpr m (x.2, id m)))))
+ = <i> comp (<_> a.1.1) (aop a (g.1 (qpr m (x.1, id m))) (g.1 (qpr m (id m, x.2))))
+ [ (i = 0) -> <j> comp (<_> a.1.1) (g.1 (qop m (qpr m (x.1, id m)) (qpr m (id m, x.2))))
+ [ (j = 0) -> g.2.1 (qpr m (x.1, id m)) (qpr m (id m, x.2))
+ , (j = 1) -> <k> g.1 (comp (<_> qgroup m) (qopeq m (x.1, id m) (id m, x.2) @ k)
+ [ (k = 0) -> <_> (qop m (qpr m (x.1, id m)) (qpr m (id m, x.2)))
+ , (k = 1) -> <l> qpr m ((hid m).2 x.1 @ l, (hid m).1 x.2 @ l) ])]
+ , (i = 1) -> <j> comp (<_> a.1.1) (aop a (g.1 (qpr m (x.1, id m))) (g.1 (qinv m (qpr m (x.2, id m)))))
+ [ (j = 0) -> <k> aop a (g.1 (qpr m (x.1, id m))) (g.1 (qinveq m (x.2, id m) @ k))
+ , (j = 1) -> <k> aop a (g.1 (qpr m (x.1, id m))) (lem_grouphom_inv (groth.1, groth.2.1) (a.1, a.2.1) g (qpr m (x.2, id m)) @ k) ]]
+ in <i> comp (<_> a.1.1) (aop a (p0 x.1 @ i) (aneg a (p0 x.2 @ i)))
+ [ (i = 0) -> <j> p1' g @ -j
+ , (i = 1) -> <j> p1' g' @ -j ]
+ p2 : Path (qgroup m -> a.1.1) g.1 g'.1
+ = <i> \ (x : qgroup m) -> setquotunivprop (pair m) (peqrel m) P p1 x @ i
+ p3 : Path (cgrouphom groth a) g g'
+ = lemSig (qgroup m -> a.1.1)
+ (ismonoidhom (groth.1, groth.2.1.1) (a.1, a.2.1.1))
+ (propismonoidhom (groth.1, groth.2.1.1) (a.1, a.2.1.1))
+ g g' p2
+ in lemSig T0 T1 pT1 x y p3
+ in (x, cntr)
+
+
+
+
+
+
T : U = (x:A) -> Path (B x) (f x) (g x)
rem1 : set T = setPi A (\ (x:A) -> Path (B x) (f x) (g x)) (\ (x:A) -> h x (f x) (g x))
+propPi2 (A : U) (B0 : A -> A -> U) (h0 : (x y : A) -> prop (B0 x y))
+ : prop ((x y : A) -> B0 x y)
+ = let
+ p0 (a : A) : prop ((b : A) -> B0 a b)
+ = propPi A (B0 a) (h0 a)
+ B1 (a : A) : U
+ = (b : A) -> B0 a b
+ in propPi A B1 p0
+
+propPi3 (A : U) (B0 : A -> A -> A -> U) (h0 : (x y z : A) -> prop (B0 x y z))
+ : prop ((x y z : A) -> B0 x y z)
+ = let
+ p0 (a b : A) : prop ((c : A) -> B0 a b c)
+ = propPi A (B0 a b) (h0 a b)
+ B1 (a b : A) : U
+ = (c : A) -> B0 a b c
+ in propPi2 A B1 p0
(\ (x : X) -> setquotunivprop X R (\ (c0 : setquot X R.1) -> P c0 (setquotpr X R x))
(\ (x0 : X) -> ps x0 x) c) c'
+setquotuniv3prop (X : U) (R : eqrel X)
+ (P : setquot X R.1 -> setquot X R.1 -> setquot X R.1 -> hProp)
+ (ps : (x0 x1 x2 : X) -> (P (setquotpr X R x0) (setquotpr X R x1) (setquotpr X R x2)).1)
+ (q0 q1 q2 : setquot X R.1) : (P q0 q1 q2).1
+ = setquotunivprop X R (P q0 q1) (\(x2' : X) -> setquotunivprop X R (\ (q1' : setquot X R.1) -> P q0 q1' (setquotpr X R x2'))
+ (\(x1' : X) -> setquotunivprop X R (\(q0' : setquot X R.1) -> P q0' (setquotpr X R x1')
+ (setquotpr X R x2')) (\(x0' : X) -> ps x0' x1' x2') q0) q1) q2
+
setsetquot (X : U) (R : hrel X) : set (setquot X R) =
setSig (hsubtypes X) (\(A : hsubtypes X) -> iseqclass X R A)
sA sB
inl _ -> true
inr _ -> false
+
+
+-- The universal property of set quotients
+
+funresprel (A B : U) (f : A -> B) (R : hrel A) : U
+ = (a a' : A) (r : (R a a').1) -> Path B (f a) (f a')
+
+-- If f respects R then all x belonging to the equivalence class C are mapped into the same unique image
+setquotmapcontr (A B : U) (sB : set B) (R : hrel A) (f : A -> B)
+ (frr : funresprel A B f R) (C : setquot A R)
+ : isContr ((y : B) * ((x : carrier A C.1) -> Path B y (f x.1)))
+ = let
+ T : U = (y : B) * ((x : carrier A C.1) -> Path B y (f x.1))
+ pT (a b : T) : Path T a b
+ = let
+ h (x : carrier A C.1) : Path B a.1 b.1 = <i> comp (<j> B) (a.2 x @ i)
+ [ (i = 0) -> <j> a.1
+ , (i = 1) -> <j> b.2 x @ -j ]
+ p0 : Path B a.1 b.1
+ = C.2.1.1 (Path B a.1 b.1, sB a.1 b.1) h
+ p1 : PathP (<i> (x : carrier A C.1) -> Path B (p0 @ i) (f x.1)) a.2 b.2
+ = let
+ P (b : B) : U
+ = (x : carrier A C.1) -> Path B b (f x.1)
+ pP (b : B) (s t : (P b)) : Path (P b) s t
+ = <i> \ (x : carrier A C.1) -> (sB b (f x.1) (s x) (t x)) @ i
+ in lemPropF B P pP a.1 b.1 p0 a.2 b.2
+ in <i> (p0 @ i, p1 @ i)
+ h (x : carrier A C.1) : T
+ = (f x.1, \ (x' : carrier A C.1) -> frr x.1 x'.1 (C.2.2 x.1 x'.1 x.2 x'.2))
+ y : T
+ = C.2.1.1 (T, pT) h
+ in (y, pT y)
+
+setquotmap (A B : U) (sB : set B) (R : hrel A) (f : A -> B)
+ (frr : funresprel A B f R) (c : setquot A R) : B
+ = (setquotmapcontr A B sB R f frr c).1.1
+
+setquotmapeq (A B : U) (sB : set B) (R : eqrel A) (f : A -> B)
+ (frr : funresprel A B f R.1) (x : A)
+ : Path B (setquotmap A B sB R.1 f frr (setquotpr A R x)) (f x)
+ = (setquotmapcontr A B sB R.1 f frr (setquotpr A R x)).1.2 (x, R.2.1.2 x)
+
+opaque setquotunivprop
+
+setquotuniversalproperty (A B : U) (sB : set B) (R : eqrel A) (f : A -> B)
+ (frr : funresprel A B f R.1)
+ : isContr ( (g : setquot A R.1 -> B)
+ * (Path (A -> B) (\ (a : A) -> g (setquotpr A R a)) f))
+ = let
+ G : U
+ = setquot A R.1 -> B
+ I (g : G) : U
+ = Path (A -> B) (\ (a : A) -> g (setquotpr A R a)) f
+ pI (g : G) : prop (I g)
+ = setPi A (\ (a : A) -> B) (\ (a : A) -> sB) (\ (a : A) -> g (setquotpr A R a)) f
+ g : G
+ = setquotmap A B sB R.1 f frr
+ i : I g
+ = <i> \ (a : A) -> setquotmapeq A B sB R f frr a @ i
+ eq (h : (g : G) * I g) : Path ((g : G) * I g) (g, i) h
+ = let
+ p0 : Path G g h.1
+ = <j> \ (x : setquot A R.1) -> let
+ P (y : setquot A R.1) : hProp
+ = (Path B (g y) (h.1 y), sB (g y) (h.1 y))
+ ps (a : A) : (P (setquotpr A R a)).1
+ = <k> comp (<_> B) ((i @ k) a)
+ [ (k = 0) -> <_> g (setquotpr A R a)
+ , (k = 1) -> <l> (h.2 @ -l) a ]
+ in setquotunivprop A R P ps x @ j
+ p1 : PathP (<i> I (p0 @ i)) i h.2
+ = lemPropF G I pI g h.1 p0 i h.2
+ in <i> (p0 @ i, p1 @ i)
+ in ((g, i), eq)
+
+funresprel2 (A B C : U) (f : A -> B -> C) (R0 : hrel A) (R1 : hrel B) : U
+ = (a a' : A) (b b' : B) -> (R0 a a').1 -> (R1 b b').1 -> Path C (f a b) (f a' b')
+
+hProppair (X Y : hProp) : hProp
+ = (and X.1 Y.1, propAnd X.1 Y.1 X.2 Y.2)
+
+hrelpair (A B : U) (R0 : hrel A) (R1 : hrel B) (x y : and A B) : hProp
+ = hProppair (R0 x.1 y.1) (R1 x.2 y.2)
+
+iseqrelpair (A B : U) (R0 : hrel A) (R1 : hrel B) (E0 : iseqrel A R0)
+ (E1 : iseqrel B R1) : iseqrel (and A B) (hrelpair A B R0 R1)
+ = let
+ T : U
+ = and A B
+ R : hrel T
+ = hrelpair A B R0 R1
+ rax : isrefl T R
+ = \ (t0 : T) -> (E0.1.2 t0.1, E1.1.2 t0.2)
+ sax : issymm T R
+ = \ (t0 t1 : T) (e : (R t0 t1).1) -> (E0.2 t0.1 t1.1 e.1, E1.2 t0.2 t1.2 e.2)
+ tax : istrans T R
+ = \ (t0 t1 t2 : T) (e0 : (R t0 t1).1) (e1 : (R t1 t2).1) ->
+ (E0.1.1 t0.1 t1.1 t2.1 e0.1 e1.1, E1.1.1 t0.2 t1.2 t2.2 e0.2 e1.2)
+ in ((tax, rax), sax)
+
+eqrelpair (A B : U) (R0 : eqrel A) (R1 : eqrel B) : eqrel (and A B)
+ = (hrelpair A B R0.1 R1.1, iseqrelpair A B R0.1 R1.1 R0.2 R1.2)
+
+hsubtypespair (A B : U) (H0 : hsubtypes A) (H1 : hsubtypes B) (x : and A B) : hProp
+ = hProppair (H0 x.1) (H1 x.2)
+
+iseqclasspair (A B : U) (R0 : hrel A) (R1 : hrel B) (H0 : hsubtypes A)
+ (H1 : hsubtypes B) (E0 : iseqclass A R0 H0) (E1 : iseqclass B R1 H1)
+ : iseqclass (and A B) (hrelpair A B R0 R1) (hsubtypespair A B H0 H1)
+ = let
+ H : hsubtypes (and A B)
+ = hsubtypespair A B H0 H1
+ a (P : hProp) (f : carrier (and A B) H -> P.1) : P.1
+ = let
+ g (x0 : carrier A H0) : P.1
+ = let
+ h (x1 : carrier B H1) : P.1
+ = f ((x0.1, x1.1), (x0.2, x1.2))
+ in E1.1.1 P h
+ in E0.1.1 P g
+ b (x0 x1 : and A B) (r : (hrelpair A B R0 R1 x0 x1).1) (h0 : (H x0).1) : (H x1).1
+ = (E0.1.2 x0.1 x1.1 r.1 h0.1, E1.1.2 x0.2 x1.2 r.2 h0.2)
+ c (x0 x1 : and A B) (h0 : (H x0).1) (h1 : (H x1).1) : (hrelpair A B R0 R1 x0 x1).1
+ = (E0.2 x0.1 x1.1 h0.1 h1.1, E1.2 x0.2 x1.2 h0.2 h1.2)
+ in ((a, b), c)
+
+setquotpair (A B : U) (R0 : hrel A) (R1 : hrel B) (q0 : setquot A R0)
+ (q1 : setquot B R1)
+ : setquot (and A B) (hrelpair A B R0 R1)
+ = ( hsubtypespair A B q0.1 q1.1
+ , iseqclasspair A B R0 R1 q0.1 q1.1 q0.2 q1.2)
+
+setquotmap2 (A B C : U) (sC : set C) (R0 : hrel A) (R1 : hrel B)
+ (f : A -> B -> C) (frr : funresprel2 A B C f R0 R1) (c0 : setquot A R0)
+ (c1 : setquot B R1) : C
+ = let
+ f' (t : and A B) : C
+ = f t.1 t.2
+ R' : hrel (and A B)
+ = hrelpair A B R0 R1
+ frr' (s t : and A B) (r : (R' s t).1) : Path C (f' s) (f' t)
+ = frr s.1 t.1 s.2 t.2 r.1 r.2
+ c' : setquot (and A B) R'
+ = setquotpair A B R0 R1 c0 c1
+ in setquotmap (and A B) C sC R' f' frr' c'
+
+setquotmapeq2 (A B C : U) (sC : set C) (R0 : eqrel A) (R1 : eqrel B)
+ (f : A -> B -> C) (frr : funresprel2 A B C f R0.1 R1.1) (x0: A) (x1 : B)
+ : Path C (setquotmap2 A B C sC R0.1 R1.1 f frr (setquotpr A R0 x0) (setquotpr B R1 x1)) (f x0 x1)
+ = let
+ f' (t : and A B) : C
+ = f t.1 t.2
+ R : eqrel (and A B)
+ = eqrelpair A B R0 R1
+ frr' (s t : and A B) (r : (R.1 s t).1) : Path C (f' s) (f' t)
+ = frr s.1 t.1 s.2 t.2 r.1 r.2
+ in setquotmapeq (and A B) C sC R f' frr' (x0, x1)
+
+transparent setquotunivprop
+
+
-- The bool exercise:
R : eqrel bool = (r1,r2)
--- /dev/null
+-- This file defines the coslice category, initial and terminal objects,
+-- universal arrows, natural transformations, and adjoint functors. It also
+-- shows that a family of universal arrows gives rise to two adjoint functors.
+module univprop where
+
+import category
+import grothendieck
+
+
+-- To show that two functors are equal it is enough to show that their object
+-- and homomorphism maps are equal
+functorId (A B : precategory) (f g : functor A B)
+ (p : Path ( (Fob : cA A -> cA B)
+ * ((x y : cA A) -> cH A x y -> cH B (Fob x) (Fob y))) (f.1, f.2.1) (g.1, g.2.1))
+ : Path (functor A B) f g
+ = let
+ T0 : U
+ = (Fob : cA A -> cA B)
+ * ((x y : cA A) -> cH A x y -> cH B (Fob x) (Fob y))
+ T1 (t : T0) : U
+ = (Fid : (x : cA A) -> Path (cH B (t.1 x) (t.1 x)) (t.2 x x (cPath A x)) (cPath B (t.1 x)))
+ * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ pT1 (t : T0) : prop (T1 t)
+ = let
+ T2 : U
+ = (x : cA A) -> Path (cH B (t.1 x) (t.1 x)) (t.2 x x (cPath A x)) (cPath B (t.1 x))
+ pT2 : prop T2
+ = propPi (cA A) (\ (x : cA A) -> Path (cH B (t.1 x) (t.1 x)) (t.2 x x (cPath A x)) (cPath B (t.1 x)))
+ (\ (x : cA A) -> cHSet B (t.1 x) (t.1 x) (t.2 x x (cPath A x)) (cPath B (t.1 x)))
+ T3 : U
+ = (x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))
+ pT3 : prop T3
+ = let
+ p0 (x y z : cA A) (f : cH A x y) (g : cH A y z) : prop (Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ = cHSet B (t.1 x) (t.1 z) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))
+ p1 (x y z : cA A) (f : cH A x y) : prop ((g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ = propPi (cH A y z)
+ (\ (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ (p0 x y z f)
+ p2 (x y z : cA A) : prop ((f : cH A x y) (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ = propPi (cH A x y)
+ (\ (f : cH A x y) -> (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ (p1 x y z)
+ in propPi3 (cA A)
+ (\ (x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Path (cH B (t.1 x) (t.1 z)) (t.2 x z (cC A x y z f g)) (cC B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)))
+ p2
+ in propAnd T2 T3 pT2 pT3
+ p0 : Path ((t : T0) * T1 t) ((f.1, f.2.1), (f.2.2.1, f.2.2.2)) ((g.1, g.2.1), (g.2.2.1, g.2.2.2))
+ = lemSig T0 T1 pT1 ((f.1, f.2.1), (f.2.2.1, f.2.2.2)) ((g.1, g.2.1), (g.2.2.1, g.2.2.2)) p
+ in <i> ((p0 @ i).1.1, (p0 @ i).1.2, (p0 @ i).2.1, (p0 @ i).2.2)
+
+
+-- The coslice category, a ↓ F
+cosliceCat (C D : precategory) (a : cA C) (F : functor D C) : precategory
+ = let
+ obj : U
+ = (y : cA D)
+ * cH C a (F.1 y)
+ hom (x y : obj) : U
+ = (h : cH D x.1 y.1)
+ * Path (cH C a (F.1 y.1)) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))
+ id (x : obj) : hom x x
+ = (cPath D x.1, <i> comp (<_> (cH C a (F.1 x.1))) (cC C a (F.1 x.1) (F.1 x.1) x.2 (F.2.2.1 x.1 @ -i))
+ [ (i = 0) -> cPathR C a (F.1 x.1) x.2
+ , (i = 1) -> <_> cC C a (F.1 x.1) (F.1 x.1) x.2 (F.2.1 x.1 x.1 (cPath D x.1)) ])
+ cmp (x y z : obj) (f : hom x y) (g : hom y z) : hom x z
+ = let
+ h : cH D x.1 z.1
+ = cC D x.1 y.1 z.1 f.1 g.1
+ p : Path (cH C a (F.1 z.1)) z.2 (cC C a (F.1 x.1) (F.1 z.1) x.2 (F.2.1 x.1 z.1 h))
+ = let
+ p2 : Path (cH C a (F.1 z.1)) z.2
+ (cC C a (F.1 y.1) (F.1 z.1) (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1))
+ = <i> comp (<_> cH C a (F.1 z.1)) (g.2 @ i)
+ [ (i = 0) -> <_> z.2
+ , (i = 1) -> <j> cC C a (F.1 y.1) (F.1 z.1) (f.2 @ j) (F.2.1 y.1 z.1 g.1) ]
+ p3 : Path (cH C a (F.1 z.1))
+ (cC C a (F.1 y.1) (F.1 z.1) (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1))
+ (cC C a (F.1 x.1) (F.1 z.1) x.2 (F.2.1 x.1 z.1 (cC D x.1 y.1 z.1 f.1 g.1)))
+ = <i> comp (<_> cH C a (F.1 z.1)) (cPathC C a (F.1 x.1) (F.1 y.1) (F.1 z.1) x.2 (F.2.1 x.1 y.1 f.1) (F.2.1 y.1 z.1 g.1) @ i)
+ [ (i = 0) -> <_> cC C a (F.1 y.1) (F.1 z.1) (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1)
+ , (i = 1) -> <j> cC C a (F.1 x.1) (F.1 z.1) x.2 (F.2.2.2 x.1 y.1 z.1 f.1 g.1 @ -j) ]
+ in <i> comp (<_> cH C a (F.1 z.1)) (p2 @ i)
+ [ (i = 0) -> <_> z.2
+ , (i = 1) -> p3 ]
+ in (h, p)
+ homSet (x y : obj) : set (hom x y)
+ = let
+ p0 : set (cH D x.1 y.1)
+ = cHSet D x.1 y.1
+ p1 (h : cH D x.1 y.1) : set (Path (cH C a (F.1 y.1)) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)))
+ = propSet ((Path (cH C a (F.1 y.1)) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))))
+ (cHSet C a (F.1 y.1) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)))
+ in setSig (cH D x.1 y.1)
+ (\ (h : cH D x.1 y.1) -> Path (cH C a (F.1 y.1)) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)))
+ p0 p1
+ homId (x y : obj) (h0 h1 : hom x y) (p : Path (cH D x.1 y.1) h0.1 h1.1)
+ : Path (hom x y) h0 h1
+ = let
+ A : U
+ = cH D x.1 y.1
+ P (h : A) : U
+ = Path (cH C a (F.1 y.1)) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))
+ pP (h : A) : prop (P h)
+ = cHSet C a (F.1 y.1) y.2 (cC C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))
+ in lemSig A P pP h0 h1 p
+ cPL (x y : obj) (f : hom x y) : Path (hom x y) (cmp x x y (id x) f) f
+ = homId x y (cmp x x y (id x) f) f (cPathL D x.1 y.1 f.1)
+ cPR (x y : obj) (f : hom x y) : Path (hom x y) (cmp x y y f (id y)) f
+ = homId x y (cmp x y y f (id y)) f (cPathR D x.1 y.1 f.1)
+ cPC (x y z w : obj) (f : hom x y) (g : hom y z) (h : hom z w)
+ : Path (hom x w) (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h))
+ = homId x w (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h)) (cPathC D x.1 y.1 z.1 w.1 f.1 g.1 h.1)
+ in ((obj, hom), id, cmp, homSet, cPL, cPR, cPC)
+
+-- Initial and terminal objects
+
+isinitial (C : precategory) (x : cA C) : U
+ = (y : cA C) -> isContr (cH C x y)
+
+initobj (C : precategory) : U
+ = (x : cA C) * isinitial C x
+
+isterminal (C : precategory) (y : cA C) : U
+ = (x : cA C) -> isContr (cH C x y)
+
+terminalobj (C : precategory) : U
+ = (y : cA C) * isinitial C y
+
+-- Universal arrow
+
+univarr (C D : precategory) (a : cA C) (F : functor D C) : U
+ = initobj (cosliceCat C D a F)
+
+-- uO : D
+uO (C D : precategory) (F : functor D C) (a : cA C) (ua : univarr C D a F) : cA D
+ = ua.1.1
+
+-- η : hom(a, F(uO))
+uEta (C D : precategory) (F : functor D C) (a : cA C) (ua : univarr C D a F)
+ : cH C a (F.1 (uO C D F a ua))
+ = ua.1.2
+
+-- ∃! hom((u0, η), y)
+uH (C D : precategory) (F : functor D C) (a : cA C) (ua : univarr C D a F) (y : cA (cosliceCat C D a F))
+ : isContr (cH (cosliceCat C D a F) ua.1 y)
+ = ua.2 y
+
+-- hom(u0, y)
+uH' (C D : precategory) (F : functor D C) (a : cA C) (ua : univarr C D a F) (y : cA (cosliceCat C D a F))
+ : cH D ua.1.1 y.1
+ = (ua.2 y).1.1
+
+-- F(uH') ∘ η = yH
+uHP (C D : precategory) (F : functor D C) (a : cA C) (ua : univarr C D a F) (y : cA (cosliceCat C D a F))
+ : Path (cH C a (F.1 y.1)) y.2
+ (cC C a (F.1 ua.1.1) (F.1 y.1) (uEta C D F a ua) (F.2.1 ua.1.1 y.1 (uH' C D F a ua y)))
+ = (ua.2 y).1.2
+
+-- A family of universal arrows gives rise to a functor.
+
+lemma_univarr_induced_functor (C D : precategory) (F : functor D C) (ua : (a : cA C) -> univarr C D a F)
+ : functor C D
+ = let
+ fob (a : cA C) : cA D
+ = uO C D F a (ua a)
+ fmor (a b : cA C) (f : cH C a b) : cH D (fob a) (fob b)
+ = uH' C D F a (ua a) (fob b, cC C a b (F.1 (fob b)) f (uEta C D F b (ua b)))
+ fid (a : cA C) : Path (cH D (fob a) (fob a)) (fmor a a (cPath C a)) (cPath D (fob a))
+ = let
+ h0 : cH (cosliceCat C D a F) (ua a).1 (ua a).1
+ = (cPath D (fob a), <i> comp (<_> cH C a (F.1 (fob a))) (cPathR C a (F.1 (fob a)) (ua a).1.2 @ -i)
+ [ (i = 0) -> <_> (ua a).1.2
+ , (i = 1) -> <j> cC C a (F.1 (fob a)) (F.1 (fob a)) (ua a).1.2 (F.2.2.1 (fob a) @ -j) ])
+ h1 : cH (cosliceCat C D a F) (ua a).1 (ua a).1
+ = let
+ y : cA (cosliceCat C D a F)
+ = (fob a, cC C a a (F.1 (fob a)) (cPath C a) (ua a).1.2)
+ h : cH D (fob a) (fob a)
+ = uH' C D F a (ua a) y
+ p : Path (cH C a (F.1 (fob a))) (ua a).1.2 (cC C a (F.1 (fob a)) (F.1 (fob a)) (ua a).1.2 (F.2.1 (fob a) (fob a) h))
+ = <i> comp (<_> cH C a (F.1 (fob a))) (cPathL C a (F.1 (fob a)) (ua a).1.2 @ -i)
+ [ (i = 0) -> <_> (ua a).1.2
+ , (i = 1) -> uHP C D F a (ua a) y ]
+ in (h, p)
+ p : Path (cH (cosliceCat C D a F) (ua a).1 (ua a).1) h0 h1
+ = <i> comp (<_> cH (cosliceCat C D a F) (ua a).1 (ua a).1) (((ua a).2 (ua a).1).2 h0 @ -i)
+ [ (i = 0) -> <_> h0
+ , (i = 1) -> ((ua a).2 (ua a).1).2 h1 ]
+ in <i> (p @ -i).1
+ fc (a b c : cA C) (f : cH C a b) (g : cH C b c)
+ : Path (cH D (fob a) (fob c)) (fmor a c (cC C a b c f g)) (cC D (fob a) (fob b) (fob c) (fmor a b f) (fmor b c g))
+ = let
+ eta_a : cH C a (F.1 (fob a))
+ = uEta C D F a (ua a)
+ eta_b : cH C b (F.1 (fob b))
+ = uEta C D F b (ua b)
+ eta_c : cH C c (F.1 (fob c))
+ = uEta C D F c (ua c)
+ x : cA (cosliceCat C D a F)
+ = (fob a, eta_a)
+ y : cA (cosliceCat C D a F)
+ = (fob c, cC C a c (F.1 (fob c)) (cC C a b c f g) eta_c)
+ z : cA (cosliceCat C D a F)
+ = (fob b, cC C a b (F.1 (fob b)) f eta_b)
+ w : cA (cosliceCat C D b F)
+ = (fob c, cC C b c (F.1 (fob c)) g eta_c)
+ h0 : cH (cosliceCat C D a F) x y
+ = let
+ h : cH D (fob a) (fob c)
+ -- = uH' C D F a (ua a) y
+ = fmor a c (cC C a b c f g)
+ p : Path (cH C a (F.1 (fob c)))
+ (cC C a c (F.1 (fob c)) (cC C a b c f g) eta_c)
+ (cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (F.2.1 (fob a) (fob c) h))
+ = uHP C D F a (ua a) y
+ in (h, p)
+ h1 : cH (cosliceCat C D a F) x y
+ = let
+ h : cH D x.1 y.1
+ -- = cC D (fob a) (fob b) (fob c) (fmor a b f) (fmor b c g)
+ = cC D (fob a) (fob b) (fob c) (uH' C D F a (ua a) z) (uH' C D F b (ua b) w)
+ p0 : Path (cH C a (F.1 (fob c)))
+ (cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (F.2.1 (fob a) (fob c) h))
+ (cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (cC C (F.1 (fob a)) (F.1 (fob b)) (F.1 (fob c))
+ (F.2.1 (fob a) (fob b) (uH' C D F a (ua a) z)) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))))
+ = <i> cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (F.2.2.2 (fob a) (fob b) (fob c) (uH' C D F a (ua a) z) (uH' C D F b (ua b) w) @ i)
+ p1 : Path (cH C a (F.1 (fob c)))
+ (cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (cC C (F.1 (fob a)) (F.1 (fob b)) (F.1 (fob c))
+ (F.2.1 (fob a) (fob b) (uH' C D F a (ua a) z)) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))))
+ (cC C a (F.1 (fob b)) (F.1 (fob c)) (cC C a (F.1 (fob a)) (F.1 (fob b)) eta_a
+ (F.2.1 (fob a) (fob b) (uH' C D F a (ua a) z))) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w)))
+ = <i> cPathC C a (F.1 (fob a)) (F.1 (fob b)) (F.1 (fob c)) eta_a (F.2.1 (fob a) (fob b) (uH' C D F a (ua a) z)) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w)) @ -i
+ p2 : Path (cH C a (F.1 (fob c)))
+ (cC C a (F.1 (fob b)) (F.1 (fob c)) (cC C a (F.1 (fob a)) (F.1 (fob b)) eta_a
+ (F.2.1 (fob a) (fob b) (uH' C D F a (ua a) z))) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w)))
+ (cC C a (F.1 (fob b)) (F.1 (fob c)) z.2 (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w)))
+ = <i> cC C a (F.1 (fob b)) (F.1 (fob c)) (uHP C D F a (ua a) z @ -i) (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))
+ p3 : Path (cH C a (F.1 (fob c)))
+ (cC C a (F.1 (fob b)) (F.1 (fob c)) z.2 (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w)))
+ (cC C a b (F.1 (fob c)) f (cC C b (F.1 (fob b)) (F.1 (fob c)) eta_b (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))))
+ = cPathC C a b (F.1 (fob b)) (F.1 (fob c)) f eta_b (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))
+ p4 : Path (cH C a (F.1 (fob c)))
+ (cC C a b (F.1 (fob c)) f (cC C b (F.1 (fob b)) (F.1 (fob c)) eta_b (F.2.1 (fob b) (fob c) (uH' C D F b (ua b) w))))
+ (cC C a b (F.1 (fob c)) f w.2)
+ = <i> cC C a b (F.1 (fob c)) f (uHP C D F b (ua b) w @ -i)
+ p5 : Path (cH C a (F.1 (fob c)))
+ (cC C a b (F.1 (fob c)) f w.2)
+ (cC C a c (F.1 (fob c)) (cC C a b c f g) eta_c)
+ = <i> cPathC C a b c (F.1 (fob c)) f g eta_c @ -i
+ p : Path (cH C a (F.1 (fob c)))
+ (cC C a c (F.1 (fob c)) (cC C a b c f g) eta_c)
+ (cC C a (F.1 (fob a)) (F.1 (fob c)) eta_a (F.2.1 (fob a) (fob c) h))
+ = <i> comp (<_> cH C a (F.1 (fob c))) (p2 @ -i)
+ [ (i = 1) -> <j> comp (<_> cH C a (F.1 (fob c))) (p1 @ -j)
+ [ (j = 0) -> <_> p1 @ 1
+ , (j = 1) -> <k> p0 @ -k ]
+ , (i = 0) -> <j> comp (<_> cH C a (F.1 (fob c))) (p4 @ j)
+ [ (j = 0) -> <k> p3 @ -k
+ , (j = 1) -> p5 ]]
+ in (h, p)
+ in <i> (comp (<_> cH (cosliceCat C D a F) x y) (((ua a).2 y).2 h0 @ -i)
+ [ (i = 0) -> <_> h0
+ , (i = 1) -> ((ua a).2 y).2 h1 ]).1
+ in (fob, fmor, fid, fc)
+
+isntrans (C D : precategory) (F G : functor C D) (eta : (x : cA C) -> cH D (F.1 x) (G.1 x))
+ : U
+ = (x y : cA C) (h : cH C x y) -> Path (cH D (F.1 x) (G.1 y))
+ (cC D (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (eta y))
+ (cC D (F.1 x) (G.1 x) (G.1 y) (eta x) (G.2.1 x y h))
+
+ntrans (C D : precategory) (F G : functor C D) : U
+ = (eta : (x : cA C) -> cH D (F.1 x) (G.1 x))
+ * (isntrans C D F G eta)
+
+ntransL (C D : precategory) (F G : functor C D) (f : ntrans C D F G) (B : precategory) (H : functor B C)
+ : ntrans B D (compFunctor B C D H F) (compFunctor B C D H G)
+ = let
+ F' : functor B D
+ = compFunctor B C D H F
+ G' : functor B D
+ = compFunctor B C D H G
+ eta (x : cA B) : cH D (F'.1 x) (G'.1 x)
+ = f.1 (H.1 x)
+ p (x y : cA B) (h : cH B x y) : Path (cH D (F'.1 x) (G'.1 y))
+ (cC D (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y))
+ (cC D (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h))
+ = f.2 (H.1 x) (H.1 y) (H.2.1 x y h)
+ in (eta, p)
+
+ntransR (C D : precategory) (F G : functor C D) (f : ntrans C D F G) (E : precategory) (H : functor D E)
+ : ntrans C E (compFunctor C D E F H) (compFunctor C D E G H)
+ = let
+ F' : functor C E
+ = compFunctor C D E F H
+ G' : functor C E
+ = compFunctor C D E G H
+ eta (x : cA C) : cH E (F'.1 x) (G'.1 x)
+ = H.2.1 (F.1 x) (G.1 x) (f.1 x)
+ p (x y : cA C) (h : cH C x y) : Path (cH E (F'.1 x) (G'.1 y))
+ (cC E (F'.1 x) (F'.1 y) (G'.1 y) (F'.2.1 x y h) (eta y))
+ (cC E (F'.1 x) (G'.1 x) (G'.1 y) (eta x) (G'.2.1 x y h))
+ = <i> comp (<_> cH E (F'.1 x) (G'.1 y)) (H.2.1 (F.1 x) (G.1 y) (f.2 x y h @ i))
+ [ (i = 0) -> H.2.2.2 (F.1 x) (F.1 y) (G.1 y) (F.2.1 x y h) (f.1 y)
+ , (i = 1) -> H.2.2.2 (F.1 x) (G.1 x) (G.1 y) (f.1 x) (G.2.1 x y h) ]
+ in (eta, p)
+
+areAdjoint (C D : precategory) (F : functor D C) (G : functor C D)
+ (unit : ntrans D D (idFunctor D) (compFunctor D C D F G))
+ (counit : ntrans C C (compFunctor C D C G F) (idFunctor C))
+ : U
+ = let
+ h0 (x : cA C) : cH D (G.1 x) (G.1 x)
+ = cC D (G.1 x) (G.1 (F.1 (G.1 x))) (G.1 x)
+ ((ntransL D D (idFunctor D) (compFunctor D C D F G) unit C G).1 x)
+ ((ntransR C C (compFunctor C D C G F) (idFunctor C) counit D G).1 x)
+ h1 (x : cA D) : cH C (F.1 x) (F.1 x)
+ = cC C (F.1 x) (F.1 (G.1 (F.1 x))) (F.1 x)
+ ((ntransR D D (idFunctor D) (compFunctor D C D F G) unit C F).1 x)
+ ((ntransL C C (compFunctor C D C G F) (idFunctor C) counit D F).1 x)
+ in and ((x : cA C) -> Path (cH D (G.1 x) (G.1 x)) (cPath D (G.1 x)) (h0 x))
+ ((x : cA D) -> Path (cH C (F.1 x) (F.1 x)) (cPath C (F.1 x)) (h1 x))
+
+adjoint (C D : precategory) (F : functor D C) (G : functor C D) : U
+ = (unit : ntrans D D (idFunctor D) (compFunctor D C D F G))
+ * (counit : ntrans C C (compFunctor C D C G F) (idFunctor C))
+ * areAdjoint C D F G unit counit
+
+lemma_univarr_unit (C D : precategory) (F : functor D C) (ua : (a : cA C) -> univarr C D a F)
+ : ntrans C C (idFunctor C) (compFunctor C D C (lemma_univarr_induced_functor C D F ua) F)
+ = let
+ f : functor C D
+ = lemma_univarr_induced_functor C D F ua
+ eta (x : cA C) : cH C x (F.1 (f.1 x))
+ = uEta C D F x (ua x)
+ in ( eta
+ , \ (x y : cA C) (h : cH C x y) -> uHP C D F x (ua x) (f.1 y, cC C x y (F.1 (f.1 y)) h (eta y)))
+
+lemma_univarr_counit (C D : precategory) (F : functor D C) (ua : (a : cA C) -> univarr C D a F)
+ : ntrans D D (compFunctor D C D F (lemma_univarr_induced_functor C D F ua)) (idFunctor D)
+ = let
+ S : functor D D
+ = compFunctor D C D F (lemma_univarr_induced_functor C D F ua)
+ T : functor D D
+ = idFunctor D
+ f : functor C D
+ = lemma_univarr_induced_functor C D F ua
+ eta (x : cA C) : cH C x (F.1 (f.1 x))
+ = uEta C D F x (ua x)
+ taF (x : cA D) : cH D (f.1 (F.1 x)) x
+ = (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x)))
+ p (x y : cA D) (h : cH D x y) : Path (cH D (S.1 x) y)
+ (cC D (S.1 x) (S.1 y) y (S.2.1 x y h) (taF y))
+ (cC D (S.1 x) x y (taF x) h)
+ = let
+ a : cA C
+ = F.1 x
+ d : cA (cosliceCat C D a F)
+ = (f.1 (F.1 x), eta (F.1 x))
+ e : cA (cosliceCat C D a F)
+ = (y, F.2.1 x y h)
+
+ -- To prove the two homomorphisms in D equal we use them to construct
+ -- two parallel homomorphisms in the coslice category. It follows from
+ -- the uniqueness property that these are equal, and by extension that the
+ -- two original homomorphisms are equal as well.
+
+ -- The construction of the first homomorphism, hom0
+ h00 : cH D (S.1 x) (S.1 y)
+ = (uH' C D F (F.1 x) (ua (F.1 x)) (f.1 (F.1 y), cC C (F.1 x) (F.1 y) (F.1 (f.1 (F.1 y))) (F.2.1 x y h) (eta (F.1 y))))
+ h01 : cH D (S.1 y) y
+ = ((uH' C D F (F.1 y) (ua (F.1 y)) (y, cPath C (F.1 y))))
+ h0 : cH D d.1 e.1
+ = cC D (S.1 x) (S.1 y) y h00 h01
+ p0 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.1 d.1 e.1 h0))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (cC C (F.1 (S.1 x)) (F.1 (S.1 y)) (F.1 y) (F.2.1 (S.1 x) (S.1 y) h00) (F.2.1 (S.1 y) y h01)))
+ = <i> cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.2.2 (S.1 x) (S.1 y) y h00 h01 @ i)
+ p1 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (cC C (F.1 (S.1 x)) (F.1 (S.1 y)) (F.1 y) (F.2.1 (S.1 x) (S.1 y) h00) (F.2.1 (S.1 y) y h01)))
+ (cC C a (F.1 (S.1 y)) (F.1 e.1) (cC C a (F.1 (S.1 x)) (F.1 (S.1 y)) (eta (F.1 x)) (F.2.1 (S.1 x) (S.1 y) h00)) (F.2.1 (S.1 y) y h01))
+ = <i> cPathC C a (F.1 d.1) (F.1 (S.1 y)) (F.1 y) (eta (F.1 x)) (F.2.1 (S.1 x) (S.1 y) h00) (F.2.1 (S.1 y) y h01) @ -i
+ p2 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 (S.1 y)) (F.1 e.1) (cC C a (F.1 (S.1 x)) (F.1 (S.1 y)) (eta (F.1 x)) (F.2.1 (S.1 x) (S.1 y) h00)) (F.2.1 (S.1 y) y h01))
+ (cC C a (F.1 (S.1 y)) (F.1 e.1) (cC C (F.1 x) (F.1 y) (F.1 (f.1 (F.1 y))) (F.2.1 x y h) (eta (F.1 y))) (F.2.1 (S.1 y) y h01))
+ = <i> (cC C a (F.1 (S.1 y)) (F.1 e.1) (uHP C D F a (ua a) (f.1 (F.1 y), cC C (F.1 x) (F.1 y) (F.1 (f.1 (F.1 y))) (F.2.1 x y h) (eta (F.1 y))) @ -i) (F.2.1 (S.1 y) y h01))
+ p3 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 (S.1 y)) (F.1 e.1) (cC C (F.1 x) (F.1 y) (F.1 (f.1 (F.1 y))) (F.2.1 x y h) (eta (F.1 y))) (F.2.1 (S.1 y) y h01))
+ (cC C a (F.1 y) (F.1 e.1) (F.2.1 x y h) (cC C (F.1 y) (F.1 (f.1 (F.1 y))) (F.1 e.1) (eta (F.1 y)) (F.2.1 (S.1 y) y h01)))
+ = cPathC C (F.1 x) (F.1 y) (F.1 (f.1 (F.1 y))) (F.1 e.1) (F.2.1 x y h) (eta (F.1 y)) (F.2.1 (S.1 y) y h01)
+ p4 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 y) (F.1 e.1) (F.2.1 x y h) (cC C (F.1 y) (F.1 (f.1 (F.1 y))) (F.1 e.1) (eta (F.1 y)) (F.2.1 (S.1 y) y h01)))
+ (cC C a (F.1 y) (F.1 e.1) (F.2.1 x y h) (cPath C (F.1 y)))
+ = <i> cC C a (F.1 y) (F.1 e.1) (F.2.1 x y h) (uHP C D F (F.1 y) (ua (F.1 y)) (y, cPath C (F.1 y)) @ -i)
+ p5 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 y) (F.1 e.1) (F.2.1 x y h) (cPath C (F.1 y)))
+ e.2
+ = cPathR C a (F.1 y) (F.2.1 x y h)
+ p : Path (cH C a (F.1 e.1)) e.2 (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.1 d.1 e.1 h0))
+ = <i> comp (<_> cH C a (F.1 e.1)) (p2 @ -i)
+ [ (i = 0) -> <j> comp (<_> cH C a (F.1 e.1)) (p4 @ j)
+ [ (j = 0) -> <k> p3 @ -k
+ , (j = 1) -> p5 ]
+ , (i = 1) -> <j> comp (<_> cH C a (F.1 e.1)) (p1 @ -j)
+ [ (j = 0) -> <_> p1 @ 1
+ , (j = 1) -> <k> p0 @ -k ] ]
+ hom0 : cH (cosliceCat C D a F) d e
+ = (h0, p)
+
+ -- The construction of the second homomorphism, hom1
+ h1 : cH D d.1 e.1
+ = (cC D (S.1 x) x y (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))) h)
+ q0 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.1 d.1 e.1 h1))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (cC C (F.1 (S.1 x)) (F.1 x) (F.1 y) (F.2.1 (S.1 x) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x)))) (F.2.1 x y h)))
+ = <i> cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.2.2 (S.1 x) x y (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))) h @ i)
+ q1 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (cC C (F.1 (S.1 x)) (F.1 x) (F.1 y) (F.2.1 (S.1 x) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x)))) (F.2.1 x y h)))
+ (cC C a (F.1 x) (F.1 e.1) (cC C a (F.1 (S.1 x)) (F.1 x) (eta (F.1 x)) (F.2.1 (S.1 x) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))))) (F.2.1 x y h))
+ = <i> cPathC C a (F.1 d.1) (F.1 x) (F.1 e.1) (eta (F.1 x)) (F.2.1 (S.1 x) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x)))) (F.2.1 x y h) @ -i
+ q2 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 x) (F.1 e.1) (cC C a (F.1 (S.1 x)) (F.1 x) (eta (F.1 x)) (F.2.1 (S.1 x) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))))) (F.2.1 x y h))
+ (cC C a (F.1 x) (F.1 e.1) (cPath C (F.1 x)) (F.2.1 x y h))
+ = <i> cC C a (F.1 x) (F.1 e.1) (uHP C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x)) @ -i) (F.2.1 x y h)
+ q3 : Path (cH C a (F.1 e.1))
+ (cC C a (F.1 x) (F.1 e.1) (cPath C (F.1 x)) (F.2.1 x y h))
+ e.2
+ = cPathL C (F.1 x) (F.1 y) (F.2.1 x y h)
+ q : Path (cH C a (F.1 e.1)) e.2 (cC C a (F.1 d.1) (F.1 e.1) (eta (F.1 x)) (F.2.1 d.1 e.1 h1))
+ = <i> comp (<_> cH C a (F.1 e.1)) (q1 @ -i)
+ [ (i = 0) -> <j> comp (<_> cH C a (F.1 e.1)) (q3 @ j)
+ [ (j = 0) -> <k> q2 @ -k
+ , (j = 1) -> <_> e.2 ]
+ , (i = 1) -> <j> q0 @ -j ]
+ hom1 : cH (cosliceCat C D a F) d e
+ = (h1, q)
+
+ -- It follows from universality that hom0 ≡ hom1
+ phom : Path (cH (cosliceCat C D a F) d e) hom0 hom1
+ = <i> comp (<_> cH (cosliceCat C D a F) d e) (uH C D F (F.1 x) (ua (F.1 x)) e).1
+ [ (i = 0) -> (uH C D F (F.1 x) (ua (F.1 x)) e).2 hom0
+ , (i = 1) -> (uH C D F (F.1 x) (ua (F.1 x)) e).2 hom1 ]
+ in <i> (phom @ i).1
+ in (taF, p)
+
+lemma_univarr_adjoint (C D : precategory) (F : functor D C) (ua : (a : cA C) -> univarr C D a F)
+ : adjoint D C (lemma_univarr_induced_functor C D F ua) F
+ = let
+ f : functor C D
+ = lemma_univarr_induced_functor C D F ua
+ eta (x : cA C) : cH C x (F.1 (f.1 x))
+ = uEta C D F x (ua x)
+ unit : ntrans C C (idFunctor C) (compFunctor C D C f F)
+ = lemma_univarr_unit C D F ua
+ counit : ntrans D D (compFunctor D C D F f) (idFunctor D)
+ = lemma_univarr_counit C D F ua
+ h0 (x : cA D) : cH C (F.1 x) (F.1 x)
+ = cC C (F.1 x) (F.1 (f.1 (F.1 x))) (F.1 x)
+ ((ntransL C C (idFunctor C) (compFunctor C D C f F) unit D F).1 x) -- (eta (F.1 x))
+ ((ntransR D D (compFunctor D C D F f) (idFunctor D) counit C F).1 x) -- (F.2.1 (f.1 (F.1 x)) x (uH' C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))))
+ p0 (x: cA D) : Path (cH C (F.1 x) (F.1 x)) (cPath C (F.1 x)) (h0 x)
+ = uHP C D F (F.1 x) (ua (F.1 x)) (x, cPath C (F.1 x))
+ h10 (x : cA C) : cH D (f.1 x) (f.1 (F.1 (f.1 x)))
+ = (uH' C D F x (ua x) (f.1 (F.1 (f.1 x)), cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x) (eta (F.1 (f.1 x)))))
+ h11 (x : cA C) : cH D (f.1 (F.1 (f.1 x))) (f.1 x)
+ = (uH' C D F (F.1 (f.1 x)) (ua (F.1 (f.1 x))) ((f.1 x), cPath C (F.1 (f.1 x))))
+ h1 (x : cA C) : cH D (f.1 x) (f.1 x)
+ = cC D (f.1 x) (f.1 (F.1 (f.1 x))) (f.1 x) (h10 x) (h11 x)
+ p1 (x: cA C) : Path (cH D (f.1 x) (f.1 x)) (cPath D (f.1 x)) (h1 x)
+ = let
+ e : cA (cosliceCat C D x F)
+ = (f.1 x, eta x)
+ h0 : cH D e.1 e.1
+ = cPath D e.1
+ hom0 : cH (cosliceCat C D x F) e e
+ = (h0, (cPath (cosliceCat C D x F) e).2)
+ p0 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (F.2.1 (f.1 x) (f.1 x) (h1 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cC C (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x))
+ (F.2.1 (f.1 x) (f.1 (F.1 (f.1 x))) (h10 x)) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))))
+ = <i> cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (F.2.2.2 (f.1 x) (f.1 (F.1 (f.1 x))) (f.1 x) (h10 x) (h11 x) @ i)
+ p1 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cC C (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x))
+ (F.2.1 (f.1 x) (f.1 (F.1 (f.1 x))) (h10 x)) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))))
+ (cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x)
+ (F.2.1 (f.1 x) (f.1 (F.1 (f.1 x))) (h10 x))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)))
+ = <i> cPathC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (eta x) (F.2.1 (f.1 x) (f.1 (F.1 (f.1 x))) (h10 x)) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)) @ -i
+ p2 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x)
+ (F.2.1 (f.1 x) (f.1 (F.1 (f.1 x))) (h10 x))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)))
+ (cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x)
+ (eta (F.1 (f.1 x)))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)))
+ = <i> cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (uHP C D F x (ua x) (f.1 (F.1 (f.1 x)), cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x) (eta (F.1 (f.1 x)))) @ -i) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))
+ p3 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x)
+ (eta (F.1 (f.1 x)))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cC C (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x))
+ (eta (F.1 (f.1 x))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))))
+ = cPathC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (eta x) (eta (F.1 (f.1 x))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))
+ p4 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cC C (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x))
+ (eta (F.1 (f.1 x))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x))))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cPath C (F.1 (f.1 x))))
+ = <i> cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (uHP C D F (F.1 (f.1 x)) (ua (F.1 (f.1 x))) ((f.1 x), cPath C (F.1 (f.1 x))) @ -i)
+ p5 : Path (cH C x (F.1 (f.1 x)))
+ (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (cPath C (F.1 (f.1 x))))
+ (eta x)
+ = cPathR C x (F.1 (f.1 x)) (eta x)
+ p : Path (cH C x (F.1 (f.1 x))) (eta x) (cC C x (F.1 (f.1 x)) (F.1 (f.1 x)) (eta x) (F.2.1 (f.1 x) (f.1 x) (h1 x)))
+ = <i> comp (<_> cH C x (F.1 (f.1 x))) (cC C x (F.1 (f.1 (F.1 (f.1 x)))) (F.1 (f.1 x)) (cC C x (F.1 (f.1 x)) (F.1 (f.1 (F.1 (f.1 x)))) (eta x)
+ (eta (F.1 (f.1 x)))) (F.2.1 (f.1 (F.1 (f.1 x))) (f.1 x) (h11 x)))
+ [ (i = 0) -> <j> comp (<_> cH C x (F.1 (f.1 x))) (p4 @ j)
+ [ (j = 0) -> <k> p3 @ -k
+ , (j = 1) -> p5 ]
+ , (i = 1) -> <j> comp (<_> cH C x (F.1 (f.1 x))) (p1 @ -j)
+ [ (j = 0) -> p2
+ , (j = 1) -> <k> p0 @ -k ]]
+ hom1 : cH (cosliceCat C D x F) e e
+ = (h1 x, p)
+ phom : Path (cH (cosliceCat C D x F) e e) hom0 hom1
+ = <i> comp (<_> cH (cosliceCat C D x F) e e) (uH C D F x (ua x) e).1
+ [ (i = 0) -> (uH C D F x (ua x) e).2 hom0
+ , (i = 1) -> (uH C D F x (ua x) e).2 hom1 ]
+ in <i> (phom @ i).1
+ in (unit, counit, p0, p1)
+
+
+CMon : precategory
+ = let
+ hom (A B : cmonoid) : U
+ = cmonoidhom A B
+ id (A : cmonoid) : hom A A
+ = idmonoidhom (A.1, A.2.1)
+ c (A B C : cmonoid) (f : hom A B) (g : hom B C) : hom A C
+ = monoidhomcomp (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) f g
+ homSet (A B : cmonoid) : set (hom A B)
+ = setmonoidhom (A.1, A.2.1) (B.1, B.2.1)
+ cPathL (A B : cmonoid) (f : hom A B) : Path (hom A B) (c A A B (id A) f) f
+ = lemma_idmonoidhom0 (A.1, A.2.1) (B.1, B.2.1) f
+ cPathR (A B : cmonoid) (f : hom A B) : Path (hom A B) (c A B B f (id B)) f
+ = lemma_idmonoidhom1 (A.1, A.2.1) (B.1, B.2.1) f
+ cPath (A B C D : cmonoid) (f : hom A B) (g : hom B C) (h : hom C D)
+ : Path (hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
+ = lemma_monoidcomp0 (A.1, A.2.1) (B.1, B.2.1) (C.1, C.2.1) (D.1, D.2.1) f g h
+ in ((cmonoid, cmonoidhom), (id, (c, (homSet, (cPathL, (cPathR, cPath))))))
+
+Ab : precategory
+ = let
+ hom (A B : cgroup) : U
+ = cgrouphom A B
+ id (A : cgroup) : hom A A
+ = idmonoidhom (A.1, A.2.1.1)
+ c (A B C : cgroup) (f : hom A B) (g : hom B C) : hom A C
+ = monoidhomcomp (A.1, A.2.1.1) (B.1, B.2.1.1) (C.1, C.2.1.1) f g
+ homSet (A B : cgroup) : set (hom A B)
+ = setmonoidhom (A.1, A.2.1.1) (B.1, B.2.1.1)
+ cPathL (A B : cgroup) (f : hom A B) : Path (hom A B) (c A A B (id A) f) f
+ = lemma_idmonoidhom0 (A.1, A.2.1.1) (B.1, B.2.1.1) f
+ cPathR (A B : cgroup) (f : hom A B) : Path (hom A B) (c A B B f (id B)) f
+ = lemma_idmonoidhom1 (A.1, A.2.1.1) (B.1, B.2.1.1) f
+ cPath (A B C D : cgroup) (f : hom A B) (g : hom B C) (h : hom C D)
+ : Path (hom A D) (c A C D (c A B C f g) h) (c A B D f (c B C D g h))
+ = lemma_monoidcomp0 (A.1, A.2.1.1) (B.1, B.2.1.1) (C.1, C.2.1.1) (D.1, D.2.1.1) f g h
+ in ((cgroup, cgrouphom), (id, (c, (homSet, (cPathL, (cPathR, cPath))))))
+
+Fforgetful : functor Ab CMon
+ = let
+ f : cgroup -> cmonoid
+ = forgetfulAb
+ Fmor (x y : cgroup) (g : cgrouphom x y) : (cmonoidhom (f x) (f y))
+ = g
+ Fid (x : cgroup)
+ : Path (cmonoidhom (f x) (f x)) (Fmor x x (idmonoidhom (x.1, x.2.1.1))) (idmonoidhom ((f x).1, (f x).2.1))
+ = <_> idmonoidhom ((f x).1, (f x).2.1)
+ p (x y z : cgroup) (g : cgrouphom x y) (h : cgrouphom y z)
+ : Path (cmonoidhom (f x) (f z))
+ (Fmor x z (monoidhomcomp (x.1, x.2.1.1) (y.1, y.2.1.1) (z.1, z.2.1.1) g h))
+ (monoidhomcomp ((f x).1, (f x).2.1) ((f y).1, (f y).2.1) ((f z).1, (f z).2.1)
+ (Fmor x y g) (Fmor y z h))
+ = <_> Fmor x z (monoidhomcomp (x.1, x.2.1.1) (y.1, y.2.1.1) (z.1, z.2.1.1) g h)
+ in (f, Fmor, Fid, p)
+
+Fgrothendieck : functor CMon Ab
+ = let
+ f : cmonoid -> cgroup
+ = grothendieck
+ Fmor (x y : cmonoid) (g : cmonoidhom x y) : (cgrouphom (f x) (f y))
+ = grothendiecklem4 x (f y)
+ (monoidhomcomp (x.1, x.2.1) (y.1, y.2.1) ((f y).1, (f y).2.1.1) g (grothendieckhom y))
+ Fid (x : cmonoid)
+ : Path (cgrouphom (f x) (f x)) (Fmor x x (idmonoidhom (x.1, x.2.1))) (idmonoidhom ((f x).1, (f x).2.1.1))
+ = let
+ i : monoidhom (x.1, x.2.1) (x.1, x.2.1)
+ = idmonoidhom (x.1, x.2.1)
+ a : cmoncgrouphom x (f x)
+ = monoidhomcomp (x.1, x.2.1) (x.1, x.2.1) ((f x).1, (f x).2.1.1) i (grothendieckhom x)
+ g : cgrouphom (f x) (f x)
+ = grothendiecklem4 x (f x) a
+ h : cgrouphom (f x) (f x)
+ = idmonoidhom ((f x).1, (f x).2.1.1)
+ P (z : (f x).1.1) : hProp
+ = ( Path (f x).1.1 (g.1 z) (h.1 z)
+ , (f x).1.2 (g.1 z) (h.1 z) )
+ ps (z : pair x) : Path (f x).1.1 (g.1 (qpr x z)) (qpr x z)
+ = <i> comp (<_> (f x).1.1) (qopeq x (z.1, id x) (id x, z.2) @ i)
+ [ (i = 0) -> <j> comp (<_> (f x).1.1) (qop x (qpr x (z.1, id x)) (qinveq x (z.2, id x) @ -j))
+ [ (j = 0) -> <_> qop x (qpr x (z.1, id x)) (qpr x (id x, z.2))
+ , (j = 1) -> <k> grothendiecklem3 x (f x) a z @ -k ]
+ , (i = 1) -> <j> qpr x ((hid x).2 z.1 @ j, (hid x).1 z.2 @ j) ]
+ p : Path ((f x).1.1 -> (f x).1.1) g.1 h.1
+ = <i> \ (z : (f x).1.1) -> (setquotunivprop (pair x) (peqrel x) P ps z @ i)
+ in lemSig ((f x).1.1 -> (f x).1.1)
+ (ismonoidhom ((f x).1, (f x).2.1.1) ((f x).1, (f x).2.1.1))
+ (propismonoidhom ((f x).1, (f x).2.1.1) ((f x).1, (f x).2.1.1))
+ g h p
+ -- A bit too slow to compile
+ p (x y z : cmonoid) (g : cmonoidhom x y) (h : cmonoidhom y z)
+ : Path (cgrouphom (f x) (f z))
+ (Fmor x z (monoidhomcomp (x.1, x.2.1) (y.1, y.2.1) (z.1, z.2.1) g h))
+ (monoidhomcomp ((f x).1, (f x).2.1.1) ((f y).1, (f y).2.1.1) ((f z).1, (f z).2.1.1)
+ (Fmor x y g) (Fmor y z h))
+ = undefined
+-- = let
+-- a0 : cmonoidhom x z
+-- = monoidhomcomp (x.1, x.2.1) (y.1, y.2.1) (z.1, z.2.1) g h
+-- a1 : cmoncgrouphom x (f z)
+-- = monoidhomcomp (x.1, x.2.1) (z.1, z.2.1) ((f z).1, (f z).2.1.1) a0 (grothendieckhom z)
+-- a2 : cgrouphom (f x) (f z)
+-- = grothendiecklem4 x (f z) a1
+-- b0 : cmoncgrouphom x (f y)
+-- = monoidhomcomp (x.1, x.2.1) (y.1, y.2.1) ((f y).1, (f y).2.1.1) g (grothendieckhom y)
+-- b1 : cgrouphom (f x) (f y)
+-- = grothendiecklem4 x (f y) b0
+-- c0 : cmoncgrouphom y (f z)
+-- = monoidhomcomp (y.1, y.2.1) (z.1, z.2.1) ((f z).1, (f z).2.1.1) h (grothendieckhom z)
+-- c1 : cgrouphom (f y) (f z)
+-- = grothendiecklem4 y (f z) c0
+-- d : cgrouphom (f x) (f z)
+-- = monoidhomcomp ((f x).1, (f x).2.1.1) ((f y).1, (f y).2.1.1) ((f z).1, (f z).2.1.1)
+-- (Fmor x y g) (Fmor y z h)
+-- P (k : (f x).1.1) : hProp
+-- = ( Path (f z).1.1 (a2.1 k) (d.1 k)
+-- , (f z).1.2 (a2.1 k) (d.1 k) )
+-- ps (k : pair x) : (P (qpr x k)).1
+-- = let
+-- q0 : Path (f z).1.1 (a2.1 (qpr x k)) (qpr z (h.1 (g.1 k.1), h.1 (g.1 k.2)))
+-- = <i> comp (<_> (f z).1.1) (qop z (qpr z (h.1 (g.1 k.1), id z)) (qinveq z (h.1 (g.1 k.2), id z) @ i))
+-- [ (i = 0) -> <j> grothendiecklem3 x (f z) a1 k @ -j
+-- , (i = 1) -> <j> comp (<_> (f z).1.1) (qopeq z (h.1 (g.1 k.1), id z) (id z, h.1 (g.1 k.2)) @ j)
+-- [ (j = 0) -> <_> qop z (qpr z (h.1 (g.1 k.1), id z)) (qpr z (id z, h.1 (g.1 k.2)))
+-- , (j = 1) -> <l> qpr z ((hid z).2 (h.1 (g.1 k.1)) @ l, (hid z).1 (h.1 (g.1 k.2)) @ l) ]]
+-- q1 : Path (f y).1.1 (b1.1 (qpr x k)) (qpr y (g.1 k.1, g.1 k.2))
+-- = <i> comp (<_> (f y).1.1) (qop y (qpr y (g.1 k.1, id y)) (qinveq y (g.1 k.2, id y) @ i))
+-- [ (i = 0) -> <j> grothendiecklem3 x (f y) b0 k @ -j
+-- , (i = 1) -> <j> comp (<_> (f y).1.1) (qopeq y (g.1 k.1, id y) (id y, g.1 k.2) @ j)
+-- [ (j = 0) -> <_> qop y (qpr y (g.1 k.1, id y)) (qpr y (id y, g.1 k.2))
+-- , (j = 1) -> <l> qpr y ((hid y).2 (g.1 k.1) @ l, (hid y).1 (g.1 k.2) @ l) ]]
+-- q2 (k : pair y) : Path (f z).1.1 (c1.1 (qpr y k)) (qpr z (h.1 k.1, h.1 k.2))
+-- = <i> comp (<_> (f z).1.1) (qop z (qpr z (h.1 k.1, id z)) (qinveq z (h.1 k.2, id z) @ i))
+-- [ (i = 0) -> <j> grothendiecklem3 y (f z) c0 k @ -j
+-- , (i = 1) -> <j> comp (<_> (f z).1.1) (qopeq z (h.1 k.1, id z) (id z, h.1 k.2) @ j)
+-- [ (j = 0) -> <_> qop z (qpr z (h.1 k.1, id z)) (qpr z (id z, h.1 k.2))
+-- , (j = 1) -> <l> qpr z ((hid z).2 (h.1 k.1) @ l, (hid z).1 (h.1 k.2) @ l) ]]
+-- q3 : Path (f z).1.1 (c1.1 (b1.1 (qpr x k))) (qpr z (h.1 (g.1 k.1), h.1 (g.1 k.2)))
+-- = <i> comp (<_> (f z).1.1) (c1.1 (q1 @ i))
+-- [ (i = 0) -> <_> c1.1 (b1.1 (qpr x k))
+-- , (i = 1) -> q2 (g.1 k.1, g.1 k.2) ]
+-- q4 : Path (f z).1.1 (c1.1 (b1.1 (qpr x k))) (qpr z (h.1 (g.1 k.1), h.1 (g.1 k.2)))
+-- = <i> comp (<_> (f z).1.1) (c1.1 (q1 @ i))
+-- [ (i = 0) -> <_> c1.1 (b1.1 (qpr x k))
+-- , (i = 1) -> q2 (g.1 k.1, g.1 k.2) ]
+-- in <i> comp (<_> (f z).1.1) (q0 @ i)
+-- [ (i = 0) -> <_> a2.1 (qpr x k)
+-- , (i = 1) -> <j> q3 @ -j ]
+-- p : Path ((f x).1.1 -> (f z).1.1) a2.1 d.1
+-- = <i> \ (k : (f x).1.1) -> (setquotprop (pair x) (peqrel x) P ps k @ i)
+-- in lemSig ((f x).1.1 -> (f z).1.1)
+-- (ismonoidhom ((f x).1, (f x).2.1.1) ((f z).1, (f z).2.1.1))
+-- (propismonoidhom ((f x).1, (f x).2.1.1) ((f z).1, (f z).2.1.1))
+-- a2 d p
+ in (f, Fmor, Fid, p)
+
+grothendieck_univarr (x : cA CMon) : univarr CMon Ab x Fforgetful
+ = ( (grothendieck x, grothendieckhom x)
+ , \ (e : cA (cosliceCat CMon Ab x Fforgetful)) -> grothendieckunivprop' x e.1 e.2)
+
+grothendieck_induced_functor : functor CMon Ab
+ = lemma_univarr_induced_functor CMon Ab Fforgetful grothendieck_univarr
+
+grothendieck_induced_functor_eq : Path (functor CMon Ab) grothendieck_induced_functor Fgrothendieck
+ = let
+ f : functor CMon Ab
+ = grothendieck_induced_functor
+ g : functor CMon Ab
+ = Fgrothendieck
+ p0 : Path (cmonoid -> cgroup) f.1 g.1
+ = <_> f.1
+ p1 : PathP (<i> (x y : cmonoid) -> cmonoidhom x y -> cgrouphom ((p0 @ i) x) ((p0 @ i) y)) f.2.1 g.2.1
+ = <_> f.2.1
+ in functorId CMon Ab f g (<i> (p0 @ i, p1 @ i))
+
+opaque grothendieck_induced_functor_eq
+
+grothendieck_adjoint : adjoint Ab CMon Fgrothendieck Fforgetful
+ = transport (<i> adjoint Ab CMon (grothendieck_induced_functor_eq @ i) Fforgetful) (lemma_univarr_adjoint CMon Ab Fforgetful grothendieck_univarr)
+
projects / cubicaltt.git / commitdiff