Show the equivalence of the different formalisms of free structures

[gelisam]

@dimecon said:

I'm currently reading about free categories and thinking more about the different formalisms. I think it'd be cool to implement different ones and show their equivalence!

[gelisam]

That does sound like a cool project! May I ask which formalisms you're reading about and from where?

Also, in the wiki page you linked to last time, they say:

In its full categorical generality, freeness isn't necessarily categorized by underlying set structure, either.

I think that might mean that the categorical formalism is more general than the stuff they covered until that point, so it might be that what I consider to be the intuitive formalism is not actually equivalent to the categorical formalism, but rather only a special case. Better not waste to much time attempting to prove something which isn't true!

[dimecon]

So to show that List A is the free monoid on the set A, we have to show a certain universal property holds, as follows. Given any function (of sets) j : A -> M, where M is a monoid, there exists a unique monoid homomorphism f : List A -> M such that f|A = j (f|A means f restricted to A). Is this the other formalism you had in mind or is it something else?

The other formalism I have in mind is this. Let G : Mon -> Set be the forgetful functor, where G (A, mappend, mempty) = a. Define the free functor to be F : Set -> Mon, where F A = (List A, _++_, nil). Then we'd want to show that F is left adjoint to G. I think this is equivalent to the above formulation. You started this for me, and I'm currently trying to work it out. It seems you're just trying to prove that toSet and toMonoid are inverses (and provide them), but in category theory, a hom-set adjunction requires that that isomorphism is natural. Is this necessary for what we are doing?

[gelisam]

in category theory, a hom-set adjunction requires that that isomorphism is natural. Is this necessary for what we are doing?

Seems like you know more category theory than I do! If the definition says so, they yes, I guess it is necessary.

Is this the other formalism you had in mind or is it something else?

Not at all! Seems like you also know more about free structures than I do :)

I didn't start form a textbook definition of free structures nor symmetric categories. Instead, I started from concrete problems similar to those outlined in the readme of category-syntax, I worked out what structures I needed in order to get what I wanted, and only then did I try to figure out whether these structures were already known. They were, and they had names like "symmetric categories".

Later on, during the implementation of category-syntax, I encountered difficulties, and once again I first worked out the structure I needed, and I again looked up to see if that structure was already known. It wasn't, but I could see that the relationship between that structure and symmetric categories was similar to the relationship between lists and monoids. So I concluded that was I was looking for was called a "free symmetric category". I still didn't know what the textbook definition of free structures was, but by looking at enough examples, I again worked out what the formal relationship between a type class and its corresponding free structure had to be.

The result of all this is that I'm working with a definition for free structures which is very intuitive to me, which works for all the examples I know of, but which nobody else seems to use. I assume it's equivalent to the official category-based definitions, but I don't understand those definitions well enough to prove it.

Anyway, without further ado, my intuitive definition is as follows.

Given a type class C on a type a, let ExpC a be the set of expressions built from values of type a and from the methods of C. The free category FreeC a is defined as the set of equivalence classes of AST a, where two expressions are considered equivalent if the laws of the C say that the two expressions should be equal.

For example, if C is Monoid, we can represent the expressions like this:

data ExpMonoid (A : Set) : Set where
  Embed : A -> ExpMonoid A
  MEmpty : ExpMonoid A
  MAppend : ExpMonoid A -> ExpMonoid A -> ExpMonoid A

And we can represent equivalence using an explicit relation:

data EquivMonoid {A : Set} : ExpMonoid A -> ExpMonoid A -> Set where
  refl : {e : ExpMonoid A}
      -> EquivMonoid e e
  sym : {e1 e2 : ExpMonoid A}
     -> EquivMonoid e1 e2 -> EquivMonoid e2 e1
  trans : {e1 e2 e3 : ExpMonoid A}
       -> EquivMonoid e1 e2
       -> EquivMonoid e2 e3
       -> EquivMonoid e1 e3
  left-id-mempty : {e : ExpMonoid A}
                -> EquivMonoid (MAppend Mempty e) e
  right-id-mempty : {e : ExpMonoid A}
                 -> EquivMonoid (MAppend e Mempty) e
  assoc-mappend : {e1 e2 e3 : ExpMonoid A}
               -> EquivMonoid (MAppend (MAppend e1 e2) e3) (MAppend e1 (MAppend e2 e3))

And then to claim that List A is an adequate representation for FreeMonoid A, we first write a function eqClass assigning each expression to its equivalence class, as represented by a value of type List A:

eqClass : {A : Set} -> ExpMonoid A -> List A

And to prove that eqClass truly does assign equivalence classes according to our equivalence relation, we need to prove that expressions which are in the same equivalence class according to eqClass are also equivalent according to the relation, and vice-versa:

sound : {A : Set}
     -> {e1 e2 : ExpMonoid A}
     -> eqClass e1 ≡ eqClass e2
     -> EquivMonoid e1 e2

complete : {A : Set}
        -> {e1 e2 : ExpMonoid A}
        -> EquivMonoid e1 e2
        -> eqClass e1 ≡ eqClass e2

[dimecon]

I think formalizing in categorical language is more complicated than I originally anticipated, but I'll think more about it. But for now, I think the intuitive equivalence class approach is more sensible and I'm going to focus on that.