From: linusbo Date: Mon, 2 Jan 2017 19:30:29 +0000 (+0100) Subject: Added definitions of algebraic structures in algstruct.ctt, a construction of the... X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=41d18c5c60b49e7fc0518d65044a11768b877e47;p=cubicaltt.git Added definitions of algebraic structures in algstruct.ctt, a construction of the Grothendieck group in grothendieck.cct, definitions of natural transformations, universal arrows, and adjunctions in univprop as well as a proof that a family of universal arrows gives rise to an adjunction. --- diff --git a/examples/README.md b/examples/README.md index 301979a..da207b9 100644 --- a/examples/README.md +++ b/examples/README.md @@ -4,6 +4,9 @@ Cubical Type Theory: examples 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 @@ -32,6 +35,9 @@ cubicaltt. The files contain: * **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 @@ -105,3 +111,9 @@ cubicaltt. The files contain: * **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. diff --git a/examples/algstruct.ctt b/examples/algstruct.ctt new file mode 100644 index 0000000..cd7af33 --- /dev/null +++ b/examples/algstruct.ctt @@ -0,0 +1,751 @@ +-- 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 + = comp (<_> g.1.1) (opGroup g (invGroup g c) (p @ i)) + [ (i = 0) -> comp (<_> g.1.1) (opGroup g ((hasInvGroup g).1 c @ j) x) + [ (j = 0) -> isAssocGroup g (invGroup g c) c x @ -k + , (j = 1) -> (hasIdGroup g).1 x ] + , (i = 1) -> comp (<_> g.1.1) (opGroup g ((hasInvGroup g).1 c @ j) y) + [ (j = 0) -> 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 + = comp (<_> g.1.1) (opGroup g (p @ i) (invGroup g c)) + [ (i = 0) -> 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) -> 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' + = comp (<_> g.1.1) (opCGroup g ((hasInvCGroup g).1 (opCGroup g a b) @ i) b') + [ (i = 1) -> (hasIdCGroup g).1 b' + , (i = 0) -> comp (<_> g.1.1) (isAssocCGroup g x' x b' @ -j) + [ (j = 0) -> <_> opCGroup g (opCGroup g x' x) b' + , (j = 1) -> comp (<_> g.1.1) (opCGroup g x' (isAssocCGroup g a b b' @ -k)) + [ (k = 0) -> <_> opCGroup g x' (opCGroup g x b') + , (k = 1) -> 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) -> opCGroup g x' ((hasIdCGroup g).2 a @ m) ]]]] + p1 : Path g.1.1 x' (opCGroup g b' a') + = comp (<_> g.1.1) (opCGroup g (p0 @ i) a') + [ (i = 1) -> <_> opCGroup g b' a' + , (i = 0) -> comp (<_> g.1.1) (isAssocCGroup g x' a a' @ -j) + [ (j = 0) -> <_> opCGroup g (opCGroup g x' a) a' + , (j = 1) -> 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 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) + = 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)) + = comp (<_> b.1.1) (f ((hasIdGroup a).1 (idGroup a) @ i)) + [ (i = 0) -> pO (idGroup a) (idGroup a) + , (i = 1) -> (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)) + = 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) + = 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) + = 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' + = 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' + = comp (<_> h.1.1) (p1 @ i) + [ (i = 0) -> opGroup h ((h.2.2.2).1 y @ j) (f.1 x') + , (i = 1) -> <_> y' ] + in 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 comp (<_> A.1) (asc a b c @ i) + [ (i = 0) -> <_> op a (op b c) + , (i = 1) -> comp (<_> A.1) (op (cm a b @ j) c) + [ (j = 0) -> <_> op (op a b) c + , (j = 1) -> 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 comp (<_> A.1) (op a (cm b c @ i)) + [ (i = 0) -> <_> op a (op b c) + , (i = 1) -> comp (<_> A.1) (swp0 A a c b @ j) + [ (j = 0) -> <_> op a (op c b) + , (j = 1) -> 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 comp (<_> A.1) (cm (op a b) c @ i) + [ (i = 0) -> <_> op (op a b) c + , (i = 1) -> 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 comp (<_> A.1) (cm (op a b) c @ i) + [ (i = 0) -> <_> op (op a b) c + , (i = 1) -> 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 comp (<_> A.1) (swp0 A a b (op c d) @ i) + [ (i = 0) -> <_> op a (op b (op c d)) + , (i = 1) -> 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 comp (<_> A.1) (swp0 A a b (op c d) @ i) + [ (i = 0) -> <_> op a (op b (op c d)) + , (i = 1) -> 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 comp (<_> A.1) (asc a b (op c d) @ -i) + [ (i = 0) -> <_> op (op a b) (op c d) + , (i = 1) -> 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 comp (<_> A.1) (asc a b (op c d) @ -i) + [ (i = 0) -> <_> op (op a b) (op c d) + , (i = 1) -> 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 comp (<_> A.1) (asc a b (op c d) @ -i) + [ (i = 0) -> <_> op (op a b) (op c d) + , (i = 1) -> 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 comp (<_> A.1) (asc a b (op c d) @ -i) + [ (i = 0) -> <_> op (op a b) (op c d) + , (i = 1) -> 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)) + = comp (<_> A.1) (swp9 A l c.2 a.1 (op k b.2) @ i) + [ (i = 0) -> op (op l c.2) (swp0 A k a.1 b.2 @ -j) + , (i = 1) -> 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)) + = comp (<_> A.1) (swp1 A (op l c.2) k (op b.1 a.2) @ i) + [ (i = 0) -> op (op l c.2) (p0 @ -j) + , (i = 1) -> 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) -> 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)) + = comp (<_> A.1) (op (op k a.2) (swp0 A l c.1 b.2 @ i)) + [ (i = 0) -> op (op k a.2) (p1 @ -j) + , (i = 1) -> swp9 A k a.2 c.1 (op l b.2) ] + in comp (<_> A.1) (p3 @ i) [ (i = 0) -> p2, (i = 1) -> p4 ] + + + diff --git a/examples/grothendieck.ctt b/examples/grothendieck.ctt new file mode 100644 index 0000000..54cb0f9 --- /dev/null +++ b/examples/grothendieck.ctt @@ -0,0 +1,626 @@ +-- 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) -> ((hid m).1 x.1 @ i, (hid m).1 x.2 @ i) + , \ (x : pair m) -> ((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) -> (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) -> (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 ( 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 ( 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) + = comp (<_> m.1.1) (op m (p0 @ i) (p1 @ i)) + [ (i = 0) -> 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) -> op m (op m k l) (swp8 (ac m) x.1 x'.2 y.1 y'.2 @ h) ] + , (i = 1) -> 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) -> 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 ( comp (<_> m.1.1) (p @ -i) + [ (i = 0) -> op m k (cm m y.1 x.2 @ j) + , (i = 1) -> 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) + = 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))) + = op m (id m) (comp ( m.1.1) (cm m (op m x.2 x.1) (id m) @ i) + [ (i = 0) -> (op m (op m x.2 x.1) (id m)) + , (i = 1) -> 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 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)) + = 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))) + = op m (id m) (comp ( m.1.1) (cm m (op m x.1 x.2) (id m) @ i) + [ (i = 0) -> (op m (op m x.1 x.2) (id m)) + , (i = 1) -> 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 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) + = qpr m ((phid m).1 x @ i) + in 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) + = qpr m ((phid m).2 x @ i) + in 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))) + = 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)) + = 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)) + = 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 comp (<_> qgroup m) (p1 @ i) + [ (i = 0) -> p0 @ -j + , (i = 1) -> 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) + = comp (<_> qgroup m) (qpr m (pcm m x0 x1 @ i)) + [ (i = 0) -> qopeq m x0 x1 @ -j + , (i = 1) -> 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) -> + comp ( g.1.1) (qopeq m (a0, id m) (a1, id m) @ -i) + [ (i = 0) -> qpr m (op m a0 a1, (hid m).1 (id m) @ j) + , (i = 1) -> (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 + = 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')) + = 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') + = 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) -> 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') + = 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) -> 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 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))) + = 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)) + = 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))) + = 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)))) + = 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) -> (agop a (g' a0) (g' a1)) + , (i = 1) -> (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))) + = comp (<_> a.1.1) (q' @ i) + [ (i = 0) -> agop a (geq a0 @ -j) (geq a1 @ -j) + , (i = 1) -> agop a (f.2.1 a0.1 a1.1 @ -j) (aginv a (f.2.1 a0.2 a1.2 @ -j)) ] + in comp (<_> a.1.1) (p @ i) + [ (i = 0) -> <_> g (agop k x0 x1) -- (g (agop k x0 x1)) + , (i = 1) -> 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))) + = \ (x : m.1.1) -> comp (<_> a.1.1) (aop a (f.1 x) (aneg a (aid a))) + [ (i = 0) -> comp (<_> a.1.1) (aop a (f.1 x) (aid a)) + [ (j = 0) -> 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) -> comp (<_> a.1.1) (aop a (f.1 x) (aneg a (f.1 (id m)))) + [ (j = 0) -> aop a (f.1 x) (aneg a (f.2.2 @ j)) + , (j = 1) -> 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))) + = comp (<_> a.1.1) (f.1 x) + [ (i = 0) -> (p @ j).1 x + , (i = 1) -> (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))))) + = comp (<_> a.1.1) (aop a (g.1 (qpr m (x.1, id m))) (g.1 (qpr m (id m, x.2)))) + [ (i = 0) -> 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) -> 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) -> qpr m ((hid m).2 x.1 @ l, (hid m).1 x.2 @ l) ])] + , (i = 1) -> 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) -> aop a (g.1 (qpr m (x.1, id m))) (g.1 (qinveq m (x.2, id m) @ k)) + , (j = 1) -> 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 comp (<_> a.1.1) (aop a (p0 x.1 @ i) (aneg a (p0 x.2 @ i))) + [ (i = 0) -> p1' g @ -j + , (i = 1) -> p1' g' @ -j ] + p2 : Path (qgroup m -> a.1.1) g.1 g'.1 + = \ (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) + + + + + + diff --git a/examples/pi.ctt b/examples/pi.ctt index 3f180ce..5cc1fa5 100644 --- a/examples/pi.ctt +++ b/examples/pi.ctt @@ -33,5 +33,22 @@ groupoidPi (A:U) (B:A -> U) (h:(x:A) -> groupoid (B x)) (f g:pi A B) : set (Path 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 diff --git a/examples/setquot.ctt b/examples/setquot.ctt index 11ad02e..1a2e7d6 100644 --- a/examples/setquot.ctt +++ b/examples/setquot.ctt @@ -183,6 +183,14 @@ setquotuniv2prop (X : U) (R : eqrel X) (P : setquot X R.1 -> setquot X R.1 -> hP (\ (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 @@ -266,6 +274,168 @@ discretetobool (X : U) (h : discrete X) (x y : X) : bool = rem (h x y) 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 = comp ( B) (a.2 x @ i) + [ (i = 0) -> a.1 + , (i = 1) -> 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 ( (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 + = \ (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 (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 + = \ (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 + = \ (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 + = comp (<_> B) ((i @ k) a) + [ (k = 0) -> <_> g (setquotpr A R a) + , (k = 1) -> (h.2 @ -l) a ] + in setquotunivprop A R P ps x @ j + p1 : PathP ( I (p0 @ i)) i h.2 + = lemPropF G I pI g h.1 p0 i h.2 + in (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) diff --git a/examples/univprop.ctt b/examples/univprop.ctt new file mode 100644 index 0000000..fb480eb --- /dev/null +++ b/examples/univprop.ctt @@ -0,0 +1,707 @@ +-- 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 ((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, 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)) + = comp (<_> cH C a (F.1 z.1)) (g.2 @ i) + [ (i = 0) -> <_> z.2 + , (i = 1) -> 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))) + = 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) -> 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 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), 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) -> 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)) + = 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 + = 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 (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)))) + = 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))) + = 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))) + = 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) + = 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) + = 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)) + = comp (<_> cH C a (F.1 (fob c))) (p2 @ -i) + [ (i = 1) -> comp (<_> cH C a (F.1 (fob c))) (p1 @ -j) + [ (j = 0) -> <_> p1 @ 1 + , (j = 1) -> p0 @ -k ] + , (i = 0) -> comp (<_> cH C a (F.1 (fob c))) (p4 @ j) + [ (j = 0) -> p3 @ -k + , (j = 1) -> p5 ]] + in (h, p) + in (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)) + = 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))) + = 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)) + = 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)) + = (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))) + = 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)) + = comp (<_> cH C a (F.1 e.1)) (p2 @ -i) + [ (i = 0) -> comp (<_> cH C a (F.1 e.1)) (p4 @ j) + [ (j = 0) -> p3 @ -k + , (j = 1) -> p5 ] + , (i = 1) -> comp (<_> cH C a (F.1 e.1)) (p1 @ -j) + [ (j = 0) -> <_> p1 @ 1 + , (j = 1) -> 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))) + = 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)) + = 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)) + = 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)) + = comp (<_> cH C a (F.1 e.1)) (q1 @ -i) + [ (i = 0) -> comp (<_> cH C a (F.1 e.1)) (q3 @ j) + [ (j = 0) -> q2 @ -k + , (j = 1) -> <_> e.2 ] + , (i = 1) -> 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 + = 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 (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)))) + = 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))) + = 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))) + = 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)))) + = 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))) + = 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) -> comp (<_> cH C x (F.1 (f.1 x))) (p4 @ j) + [ (j = 0) -> p3 @ -k + , (j = 1) -> p5 ] + , (i = 1) -> comp (<_> cH C x (F.1 (f.1 x))) (p1 @ -j) + [ (j = 0) -> p2 + , (j = 1) -> 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 + = 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 (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) + = comp (<_> (f x).1.1) (qopeq x (z.1, id x) (id x, z.2) @ i) + [ (i = 0) -> 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) -> grothendiecklem3 x (f x) a z @ -k ] + , (i = 1) -> 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 + = \ (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))) +-- = 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) -> grothendiecklem3 x (f z) a1 k @ -j +-- , (i = 1) -> 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) -> 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)) +-- = 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) -> grothendiecklem3 x (f y) b0 k @ -j +-- , (i = 1) -> 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) -> 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)) +-- = 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) -> grothendiecklem3 y (f z) c0 k @ -j +-- , (i = 1) -> 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) -> 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))) +-- = 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))) +-- = 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 comp (<_> (f z).1.1) (q0 @ i) +-- [ (i = 0) -> <_> a2.1 (qpr x k) +-- , (i = 1) -> q3 @ -j ] +-- p : Path ((f x).1.1 -> (f z).1.1) a2.1 d.1 +-- = \ (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 ( (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 ( (p0 @ i, p1 @ i)) + +opaque grothendieck_induced_functor_eq + +grothendieck_adjoint : adjoint Ab CMon Fgrothendieck Fforgetful + = transport ( adjoint Ab CMon (grothendieck_induced_functor_eq @ i) Fforgetful) (lemma_univarr_adjoint CMon Ab Fforgetful grothendieck_univarr) +