Added goodSingleton and goodPermutation

Author: sjoerdvisscher

src/Cartographer/GoodHypergraphCategory.idr

@@ -43,6 +43,12 @@ goodHypergraphCat {o} sigma arityIn arityOut = MkCategory
   (\a, b, (Element g gg) => subsetEq (hgRightId a b g))
   (\a, b, c, d, (Element f ff), (Element g gg), (Element h hh) => subsetEq (hgAssoc a b c d f g h))
 
+goodSingleton : {s : Type} -> {ai, ao : s -> List o} -> (edge : s) -> mor (goodHypergraphCat s ai ao) (ai edge) (ao edge)
+goodSingleton x = Element (Hypergraph.singleton x) (Singleton x)
+
+goodPermutation : {s : Type} -> {ai, ao : s -> List o} -> Perm k m -> mor (goodHypergraphCat s ai ao) k m
+goodPermutation p = Element (permutation p) (Permutation p)
+
 goodHyperGraphTensor : (s : Type) -> (ai, ao : s -> List o) -> CFunctor (productCategory (goodHypergraphCat s ai ao) (goodHypergraphCat s ai ao)) (goodHypergraphCat s ai ao)
 goodHyperGraphTensor s ai ao = MkCFunctor
   (\a => fst a ++ snd a)

src/PetriGraph.idr

@@ -113,6 +113,5 @@ goodMapping s (Sequence x y) {k} = do
                   in pure $ compose (cat (goodPetriSMC s)) _ _ _ x' y''
        No _ => Nothing
 goodMapping s (Id x) = Just $ identity (cat (goodPetriSMC s)) [x]
-goodMapping s (Sym a b) = Just $ Element (permutation (swap [a] [b]))
-  (GoodHypergraphCategory.Permutation (Ins (Ins Nil HereS) (ThereS HereS)))
-goodMapping s (Mor x) = Just $ Element (Hypergraph.singleton x) (Singleton x)
+goodMapping s (Sym a b) = Just $ goodPermutation (swap [a] [b])
+goodMapping s (Mor x) = Just $ goodSingleton x