module swaptrans where import bishop import algebra import subtype 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (asc a b c @ i) [ (i = 0) -> <_> opm a (opm b c) , (i = 1) -> comp (<_> A.1) (opm (cm a b @ j) c) [ (j = 0) -> <_> opm (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (opm a (cm b c @ i)) [ (i = 0) -> <_> opm a (opm b c) , (i = 1) -> comp (<_> A.1) (swp0 A a c b @ j) [ (j = 0) -> <_> opm a (opm c b) , (j = 1) -> opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (cm (opm a b) c @ i) [ (i = 0) -> <_> opm (opm a b) c , (i = 1) -> comp (<_> A.1) (swp0 A c a b @ j) [ (j = 0) -> <_> opm c (opm a b) , (j = 1) -> cm a (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (cm (opm a b) c @ i) [ (i = 0) -> <_> opm (opm a b) c , (i = 1) -> comp (<_> A.1) (swp1 A c a b @ j) [ (j = 0) -> <_> opm c (opm a b) , (j = 1) -> cm b (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (swp0 A a b (opm c d) @ i) [ (i = 0) -> <_> opm a (opm b (opm c d)) , (i = 1) -> comp (<_> A.1) (opm b (swp0 A a c d @ j)) [ (j = 0) -> <_> (opm b (opm a (opm c d))) , (j = 1) -> swp0 A b c (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (swp0 A a b (opm c d) @ i) [ (i = 0) -> <_> opm a (opm b (opm c d)) , (i = 1) -> comp (<_> A.1) (opm b (swp1 A a c d @ j)) [ (j = 0) -> <_> (opm b (opm a (opm c d))) , (j = 1) -> swp0 A b d (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (asc a b (opm c d) @ -i) [ (i = 0) -> <_> opm (opm a b) (opm c d) , (i = 1) -> comp (<_> A.1) (swp4 A a b c d @ j) [ (j = 0) -> <_> (opm a (opm b (opm c d))) , (j = 1) -> asc c b (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (asc a b (opm c d) @ -i) [ (i = 0) -> <_> opm (opm a b) (opm c d) , (i = 1) -> comp (<_> A.1) (swp5 A a b c d @ j) [ (j = 0) -> <_> (opm a (opm b (opm c d))) , (j = 1) -> asc d b (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (asc a b (opm c d) @ -i) [ (i = 0) -> <_> opm (opm a b) (opm c d) , (i = 1) -> comp (<_> A.1) (opm a (swp0 A b c d @ j)) [ (j = 0) -> <_> (opm a (opm b (opm c d))) , (j = 1) -> asc a c (opm 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 opm : A.1 -> A.1 -> A.1 = A.2.1 asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y in comp (<_> A.1) (asc a b (opm c d) @ -i) [ (i = 0) -> <_> opm (opm a b) (opm c d) , (i = 1) -> comp (<_> A.1) (opm a (swp1 A b c d @ j)) [ (j = 0) -> <_> (opm a (opm b (opm c d))) , (j = 1) -> asc a d (opm c b) ]] swptrans (A : AscCom) (k l : A.1) (a b c : prod 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 opm : A.1 -> A.1 -> A.1 = A.2.1 op3 (x y z : A.1) : A.1 = opm x (opm y z) asc (x y z : A.1) : Path A.1 (opm x (opm y z)) (opm (opm x y) z) = A.2.2.1 x y z cm (x y : A.1) : Path A.1 (opm x y) (opm y x) = A.2.2.2 x y p2 : Path A.1 (opm (opm l c.2) (op3 k a.1 b.2)) (opm (op3 k l b.2) (opm a.1 c.2)) = comp (<_> A.1) (swp9 A l c.2 a.1 (opm k b.2) @ i) [ (i = 0) -> opm (opm l c.2) (swp0 A k a.1 b.2 @ -j) , (i = 1) -> opm (swp0 A l k b.2 @ j) (opm a.1 c.2) ] p3 : Path A.1 (opm (opm l c.2) (op3 k a.1 b.2)) (opm (opm k a.2) (op3 l b.1 c.2)) = comp (<_> A.1) (swp1 A (opm l c.2) k (opm b.1 a.2) @ i) [ (i = 0) -> opm (opm l c.2) (p0 @ -j) , (i = 1) -> comp (<_> A.1) (swp6 A b.1 a.2 k (opm l c.2) @ j) [ (j = 0) -> <_> opm (opm b.1 a.2) (op3 k l c.2) , (j = 1) -> opm (opm k a.2) (swp0 A b.1 l c.2 @ m) ]] p4 : Path A.1 (opm (opm k a.2) (op3 l b.1 c.2)) (opm (op3 k l b.2) (opm c.1 a.2)) = comp (<_> A.1) (opm (opm k a.2) (swp0 A l c.1 b.2 @ i)) [ (i = 0) -> opm (opm k a.2) (p1 @ -j) , (i = 1) -> swp9 A k a.2 c.1 (opm l b.2) ] in comp (<_> A.1) (p3 @ i) [ (i = 0) -> p2, (i = 1) -> p4 ] -- commuative monoids and groups opm (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) -> opm m a (opm m b c) asc (m: cmonoid): isAssociative m.1.1 (opm m) = isAssocCMonoid m idm (m: cmonoid): m.1.1 = idCMonoid m hid (m: cmonoid): hasIdentity m.1.1 (opm m) (idm m) = hasIdCMonoid m cm (m: cmonoid): isCommutative m.1.1 (opm m) = isCommCMonoid m ac (m: cmonoid): AscCom = (m.1.1, opm m, asc m, cm m) gac (g: abgroup): 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 = prod m.1.1 m.1.1 pset (m: cmonoid): isSet (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 = (opm m x.1 y.1, opm m x.2 y.2) pid (m: cmonoid): pair m = (idm m, idm 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) --------------------------- prel (m: cmonoid) (a b : pair m): PROP = exists m.1.1 (\(t: m.1.1) -> Path m.1.1 (op3 m t a.1 b.2) (op3 m t b.1 a.2)) 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 = idm m in existspr m.1.1 T k ( opm m (idm m) (opm 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 : PROP = 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 (opm m k (opm 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))