Skip to content

Commit a1ce347

Browse files
sjoerdvisschersjoerdvisscher
committed
WIP
1 parent 17a8ef8 commit a1ce347

File tree

3 files changed

+110
-92
lines changed

3 files changed

+110
-92
lines changed

‎src/Permutations/Permutations.idr‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,10 @@ data Perm : {o : Type} -> List o -> List o -> Type where
99
Nil : Perm [] []
1010
Ins : Perm xs ys -> SwapDown (a::ys) zs -> Perm (a::xs) zs
1111

12+
Uninhabited (Perm (x::xs) []) where
13+
uninhabited Nil impossible
14+
uninhabited (Ins _ sd) = uninhabited sd
15+
1216
insInjective: Ins {ys=ys1} p1 s1 = Ins {ys=ys2} p2 s2 -> (ys1 = ys2, p1 = p2, s1 = s2)
1317
insInjective Refl = (Refl, Refl, Refl)
1418

‎src/Permutations/PermutationsStrictMonoidalCategory.idr‎

Lines changed: 102 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,9 @@ permAddNilRightNeutral {as=a::as1} {bs} (Ins {ys} p s) =
3838
(permAddNilRightNeutral p)
3939
(appendedNilNeutral s)
4040

41+
magic : {ys : List t} -> SwapDown (a1 :: ys) cs1 -> List t
42+
magic _ {ys} = ys
43+
4144
permPreserveCompose : (a, b, c : (List o, List o))
4245
-> (f : ProductMorphism (permutationsCat o) (permutationsCat o) a b)
4346
-> (g : ProductMorphism (permutationsCat o) (permutationsCat o) b c)
@@ -51,95 +54,102 @@ permPreserveCompose (as, _) (bs, _) (cs, _) (MkProductMorphism f1 Nil) (MkProduc
5154
(sym $ appendNilRightNeutral cs)
5255
(sym $ permAddNilRightNeutral f1)
5356
(sym $ permAddNilRightNeutral g1)
54-
permPreserveCompose (a1::as1, a2::as2) (bs1, bs2) (cs1, cs2)
55-
(MkProductMorphism (Ins pf1 sf1) (Ins pf2 sf2)) (MkProductMorphism g1 g2) = ?y
56-
57-
permTensor : (o : Type) -> CFunctor (productCategory (permutationsCat o) (permutationsCat o)) (permutationsCat o)
58-
permTensor _ = MkCFunctor
59-
(\a => fst a ++ snd a)
60-
(\a, b, f => permAdd (pi1 f) (pi2 f) {as=fst a} {bs=fst b} {cs=snd a} {ds=snd b})
61-
(\a => permPreserveId (fst a) (snd a))
62-
permPreserveCompose
63-
64-
permAddAssociativeMor : (pab : Perm as bs) -> (pcd : Perm cs ds) -> (pef : Perm es fs)
65-
-> permAdd pab (permAdd pcd pef) = permAdd (permAdd pab pcd) pef
66-
permAddAssociativeMor Nil _ _ = Refl
67-
permAddAssociativeMor {as=a::as} {bs} {cs} {ds} {es} {fs} (Ins {ys} pab s) pcd pef = insCong5
68-
(appendAssociative as cs es)
69-
(appendAssociative ys ds fs)
70-
(appendAssociative bs ds fs)
71-
(permAddAssociativeMor pab pcd pef)
72-
(appendedAppendDistr ds fs s)
73-
74-
permutationsSMC : (o : Type) -> StrictMonoidalCategory
75-
permutationsSMC o = MkStrictMonoidalCategory
76-
(permutationsCat o)
77-
(permTensor o)
78-
[]
79-
(\as => Refl)
80-
(\as => appendNilRightNeutral as)
81-
appendAssociative
82-
(\_, _, _, _, _, _ => permAddAssociativeMor)
83-
84-
85-
-- for symmetric monoidal category
86-
swapAddEq : (as, bs, cs : List o) -> swapAddIdR as bs cs = swap as bs `permAdd` permId cs
87-
swapAddEq [] [] cs = Refl
88-
swapAddEq [] bs cs = sym (permPreserveId bs cs) `trans` permAddCong6 Refl (sym $ appendNilRightNeutral bs) Refl Refl (rewriteRightIgnoreR Refl) Refl
89-
swapAddEq (a::as) bs cs = insCong5 (appendAssociative as bs cs) (appendAssociative bs as cs) (appendAssociative bs (a::as) cs) (swapAddEq as bs cs) (swapDownAppendedNeutral bs _ cs)
90-
91-
swapNilRightNeutral : (l : List o) -> swap l [] = permId l
92-
swapNilRightNeutral [] = Refl
93-
swapNilRightNeutral (l::ls) = insCong5 (appendNilRightNeutral ls) Refl Refl (swapNilRightNeutral ls) Refl
94-
95-
swapAddIdRNilRightNeutral : (l : List o) -> (k : List o) -> swapAddIdR l [] k = permId (l ++ k)
96-
swapAddIdRNilRightNeutral [] k = Refl
97-
swapAddIdRNilRightNeutral (l::ls) k = insCong5 Refl Refl Refl (swapAddIdRNilRightNeutral ls k) Refl
98-
99-
--\/----- --\/---}
100-
--/\-\/-- = {--/\/--}
101-
-----/\-- {---/\--
102-
swapHexagonal1 : (as, bs, cs : List o) ->
103-
swapAddIdR as bs cs `permComp` permAddIdL bs (swap as cs) = swap as (bs ++ cs)
104-
105-
swapHexagonal1' : (as, bs, cs, ds : List o) ->
106-
swapAddIdR as bs (cs ++ ds) `permComp` permAddIdL bs (swapAddIdR as cs ds) = swapAddIdR as (bs ++ cs) ds
107-
108-
-----\/-- {---\/--
109-
--\/-/\-- = {--\/\--}
110-
--/\----- --/\---}
111-
swapHexagonal2 : (as, bs, cs : List o) ->
112-
permAddIdL as (swap bs cs) `permComp` swapAddIdR as cs bs = swap (as ++ bs) cs
113-
114-
swapHexagonal2' : (as, bs, cs, ds : List o) ->
115-
permAddIdL as (swapAddIdR bs cs ds) `permComp` swapAddIdR as cs (bs ++ ds) = swapAddIdR (as ++ bs) cs ds
116-
117-
--p-\/-- = --\/----
118-
----/\-- --/\-p--
119-
swapNatural : (as, bs, cs : List o) -> (p : Perm as bs) ->
120-
(p `permAdd` permId cs) `permComp` swap bs cs = swap as cs `permComp` permAddIdL cs p
121-
122-
swapNatural' : (as, bs, cs, ds : List o) -> (p : Perm as bs) ->
123-
(p `permAdd` permId (cs ++ ds)) `permComp` swapAddIdR bs cs ds = swapAddIdR as cs ds `permComp` permAddIdL cs (p `permAdd` permId ds)
124-
125-
-----\/----- --\/----\/--
126-
--\/-/\-\/-- = --/\-\/-/\--
127-
--/\----/\-- -----/\-----
128-
swap3' : (as, bs, cs, ds : List o)
129-
-> (permAddIdL as (swapAddIdR bs cs ds) `permComp` swapAddIdR as cs (bs ++ ds)) `permComp` permAddIdL cs (swapAddIdR as bs ds)
130-
= swapAddIdR as bs (cs ++ ds) `permComp` (permAddIdL bs (swapAddIdR as cs ds) `permComp` swapAddIdR bs cs (as ++ ds))
131-
swap3' as bs cs ds =
132-
trans (permCompCong5 (appendAssociative as bs (cs ++ ds))
133-
(cong {f=\z=>cs++z} (appendAssociative as bs ds))
134-
(cong {f=\z=>cs++z} (appendAssociative bs as ds))
135-
(swapHexagonal2' as bs cs ds)
136-
(permAddIdLCong4 Refl
137-
(appendAssociative as bs ds)
138-
(appendAssociative bs as ds)
139-
(swapAddEq as bs ds)))
140-
(trans (sym $ swapNatural' (as ++ bs) (bs ++ as) cs ds (swap as bs))
141-
(permCompCong5 (sym $ appendAssociative as bs (cs ++ ds))
142-
(sym $ appendAssociative bs as (cs ++ ds))
143-
(cong {f=\z=>cs++z} (sym $ appendAssociative bs as ds))
144-
(sym $ swapAddEq as bs (cs ++ ds))
145-
(sym $ swapHexagonal2' bs as cs ds)))
57+
permPreserveCompose (a1::as1, a2::as2) ([], []) (cs1,cs2) (MkProductMorphism f1 f2) (MkProductMorphism g1 g2) = absurd f1
58+
permPreserveCompose (a1::as1, as2) (a1::ys1, bs2) (cs1, cs2)
59+
(MkProductMorphism (Ins pf1 HereS) fs) (MkProductMorphism (Ins g1 gs1) gs) {o} = cong
60+
{f=\x => Ins x (appended cs2 gs1)} $
61+
permPreserveCompose (as1, as2) (ys1, bs2) (magic {t=o} gs1, cs2) (MkProductMorphism pf1 fs) (MkProductMorphism g1 gs)
62+
permPreserveCompose (a1::as1, as2) (b1::bs1, bs2) (cs1, cs2)
63+
(MkProductMorphism (Ins pf1 (ThereS fs1)) fs) (MkProductMorphism (Ins g1 gs1) gs) {o} = ?y1
64+
permPreserveCompose (as1, a2::as2) (bs1, b2::bs2) (cs1, cs2)
65+
(MkProductMorphism fs (Ins pf2 sf2)) (MkProductMorphism gs (Ins pg2 sg2)) = ?y2
66+
67+
-- permTensor : (o : Type) -> CFunctor (productCategory (permutationsCat o) (permutationsCat o)) (permutationsCat o)
68+
-- permTensor _ = MkCFunctor
69+
-- (\a => fst a ++ snd a)
70+
-- (\a, b, f => permAdd (pi1 f) (pi2 f) {as=fst a} {bs=fst b} {cs=snd a} {ds=snd b})
71+
-- (\a => permPreserveId (fst a) (snd a))
72+
-- permPreserveCompose
73+
74+
-- permAddAssociativeMor : (pab : Perm as bs) -> (pcd : Perm cs ds) -> (pef : Perm es fs)
75+
-- -> permAdd pab (permAdd pcd pef) = permAdd (permAdd pab pcd) pef
76+
-- permAddAssociativeMor Nil _ _ = Refl
77+
-- permAddAssociativeMor {as=a::as} {bs} {cs} {ds} {es} {fs} (Ins {ys} pab s) pcd pef = insCong5
78+
-- (appendAssociative as cs es)
79+
-- (appendAssociative ys ds fs)
80+
-- (appendAssociative bs ds fs)
81+
-- (permAddAssociativeMor pab pcd pef)
82+
-- (appendedAppendDistr ds fs s)
83+
84+
-- permutationsSMC : (o : Type) -> StrictMonoidalCategory
85+
-- permutationsSMC o = MkStrictMonoidalCategory
86+
-- (permutationsCat o)
87+
-- (permTensor o)
88+
-- []
89+
-- (\as => Refl)
90+
-- (\as => appendNilRightNeutral as)
91+
-- appendAssociative
92+
-- (\_, _, _, _, _, _ => permAddAssociativeMor)
93+
94+
95+
-- -- for symmetric monoidal category
96+
-- swapAddEq : (as, bs, cs : List o) -> swapAddIdR as bs cs = swap as bs `permAdd` permId cs
97+
-- swapAddEq [] [] cs = Refl
98+
-- swapAddEq [] bs cs = sym (permPreserveId bs cs) `trans` permAddCong6 Refl (sym $ appendNilRightNeutral bs) Refl Refl (rewriteRightIgnoreR Refl) Refl
99+
-- swapAddEq (a::as) bs cs = insCong5 (appendAssociative as bs cs) (appendAssociative bs as cs) (appendAssociative bs (a::as) cs) (swapAddEq as bs cs) (swapDownAppendedNeutral bs _ cs)
100+
101+
-- swapNilRightNeutral : (l : List o) -> swap l [] = permId l
102+
-- swapNilRightNeutral [] = Refl
103+
-- swapNilRightNeutral (l::ls) = insCong5 (appendNilRightNeutral ls) Refl Refl (swapNilRightNeutral ls) Refl
104+
105+
-- swapAddIdRNilRightNeutral : (l : List o) -> (k : List o) -> swapAddIdR l [] k = permId (l ++ k)
106+
-- swapAddIdRNilRightNeutral [] k = Refl
107+
-- swapAddIdRNilRightNeutral (l::ls) k = insCong5 Refl Refl Refl (swapAddIdRNilRightNeutral ls k) Refl
108+
109+
-- --\/----- --\/---}
110+
-- --/\-\/-- = {--/\/--}
111+
-- -----/\-- {---/\--
112+
-- swapHexagonal1 : (as, bs, cs : List o) ->
113+
-- swapAddIdR as bs cs `permComp` permAddIdL bs (swap as cs) = swap as (bs ++ cs)
114+
115+
-- swapHexagonal1' : (as, bs, cs, ds : List o) ->
116+
-- swapAddIdR as bs (cs ++ ds) `permComp` permAddIdL bs (swapAddIdR as cs ds) = swapAddIdR as (bs ++ cs) ds
117+
118+
-- -----\/-- {---\/--
119+
-- --\/-/\-- = {--\/\--}
120+
-- --/\----- --/\---}
121+
-- swapHexagonal2 : (as, bs, cs : List o) ->
122+
-- permAddIdL as (swap bs cs) `permComp` swapAddIdR as cs bs = swap (as ++ bs) cs
123+
124+
-- swapHexagonal2' : (as, bs, cs, ds : List o) ->
125+
-- permAddIdL as (swapAddIdR bs cs ds) `permComp` swapAddIdR as cs (bs ++ ds) = swapAddIdR (as ++ bs) cs ds
126+
127+
-- --p-\/-- = --\/----
128+
-- ----/\-- --/\-p--
129+
-- swapNatural : (as, bs, cs : List o) -> (p : Perm as bs) ->
130+
-- (p `permAdd` permId cs) `permComp` swap bs cs = swap as cs `permComp` permAddIdL cs p
131+
132+
-- swapNatural' : (as, bs, cs, ds : List o) -> (p : Perm as bs) ->
133+
-- (p `permAdd` permId (cs ++ ds)) `permComp` swapAddIdR bs cs ds = swapAddIdR as cs ds `permComp` permAddIdL cs (p `permAdd` permId ds)
134+
135+
-- -----\/----- --\/----\/--
136+
-- --\/-/\-\/-- = --/\-\/-/\--
137+
-- --/\----/\-- -----/\-----
138+
-- swap3' : (as, bs, cs, ds : List o)
139+
-- -> (permAddIdL as (swapAddIdR bs cs ds) `permComp` swapAddIdR as cs (bs ++ ds)) `permComp` permAddIdL cs (swapAddIdR as bs ds)
140+
-- = swapAddIdR as bs (cs ++ ds) `permComp` (permAddIdL bs (swapAddIdR as cs ds) `permComp` swapAddIdR bs cs (as ++ ds))
141+
-- swap3' as bs cs ds =
142+
-- trans (permCompCong5 (appendAssociative as bs (cs ++ ds))
143+
-- (cong {f=\z=>cs++z} (appendAssociative as bs ds))
144+
-- (cong {f=\z=>cs++z} (appendAssociative bs as ds))
145+
-- (swapHexagonal2' as bs cs ds)
146+
-- (permAddIdLCong4 Refl
147+
-- (appendAssociative as bs ds)
148+
-- (appendAssociative bs as ds)
149+
-- (swapAddEq as bs ds)))
150+
-- (trans (sym $ swapNatural' (as ++ bs) (bs ++ as) cs ds (swap as bs))
151+
-- (permCompCong5 (sym $ appendAssociative as bs (cs ++ ds))
152+
-- (sym $ appendAssociative bs as (cs ++ ds))
153+
-- (cong {f=\z=>cs++z} (sym $ appendAssociative bs as ds))
154+
-- (sym $ swapAddEq as bs (cs ++ ds))
155+
-- (sym $ swapHexagonal2' bs as cs ds)))

‎src/Permutations/SwapDown.idr‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ data SwapDown : List t -> List t -> Type where
77
HereS : SwapDown (a::as) (a::as)
88
ThereS : SwapDown (a::as) bs -> SwapDown (a::b::as) (b::bs)
99

10+
Uninhabited (SwapDown (x::xs) []) where
11+
uninhabited HereS impossible
12+
uninhabited (ThereS _) impossible
13+
1014
congHereS : (as1 = as2) -> (HereS {a} {as=as1} = HereS {a} {as=as2})
1115
congHereS Refl = Refl
1216

0 commit comments

Comments
 (0)