On the need for "funext" in agda-algebras

One of the large sources of "funext" is this definition

agda-algebras/UniversalAlgebra/Relations/Discrete.lagda

Lines 77 to 79 in 5a5687e

    
           --The type of operations 
        
           Op : Type 𝓥 → Type 𝓤 → Type(𝓤 ⊔ 𝓥) 
        
           Op I A = (I → A) → A

of Op.

In theory, I like it a lot. That one can model arity by an arbitrary type, instead of involving Fin n, is one of the really elegant things in this library. So I definitely want to preserve the design decision that we can have I-ary operation symbols.

However, the design decision to model these as Agda functions is a source of problems. If Fin n was used, for example, and then operation symbols modeled with Vec A n, all such uses [wd: of funext (?)] would go away. That does seem too drastic a move.

What seems to be needed is an abstract notion of arity and representation of I-ary operation, with an explicit getter. Then one could define an explicit equality for these easily enough. Of course, that gets us into the land of Setoid.

This may not be so bad: agda-stdlib is mostly Setoid-based already. And, this also helps with quotients!

My recommendation would be that, for this version of the library, things should be based on Setoid instead of propositional equality. Yet another version should probably exist in cubical-agda that would make radically different choices (appropriately so).

This is an interesting and important issue and your comments are very helpful. Thank you! I would definitely like to see you implement a getter and then use that to avoid using funext somehow. That would be cool! An alternative that I think I will implement today, along side the general Op type, is an operation type with countable arity. I need to start using this for my current research in complexity theory asap! In my research even Fin n arity would do, but I haven't enjoyed working with the Fin type. (Nat is so much easier for me... but that's my fault and I need to eventually make peace with the Fins. :) So, for now, it is most expedient for me to encode operations with countable arity, I think. Will such a type let us get away without funext? Overall, I agree with your recommendations. We should keep things standard and Setoid-based in this version and have a separate cubical version.

Actually, what I need right now (if not yesterday!) for my work are relational structures, as well as structures with general signatures (i.e., signatures with both relation symbols and operation symbols). I had started working on a version called "cubical-structures." But I'm realizing that translating to cubical will take too long for the short term goals of my current research, so I suppose I'll quickly cobble together another library, similar to agda-algebras, but with general (relational-algebraic) signatures.
I guess I'll call it agda-model-theory.

Unless... do you think we should incorporate this into agda-algebras? I think the general signatures will be much more complicated to work with, so I'm more inclined to make this a separate library.

Also, do you happen to know of other good model theory formalizations? Can you tell me if agda-categories already formalizes much theory of relational and general structures?

Of course, the relations in the standard library (e.g., here) won't do, since they're much too special---not only are the relations' arities fixed, they are limited to 0, 1, or 2! ...but maybe I'm just not looking in the right places for existing formalizations...?

Let me try to address all of the items in turn.

Using an abstract interface would not let us escape funext on its own, unfortunately. The abstract interface would need to export a notion of equality for that, but to access that externally would be to forgo using propositional equality in a number of places - which puts us squarely in Setoid land. So I'm glad you're ok without doing that. In fact, via Setoid, one can keep the definition of I-ary Op as is, and just change equality to pointwise!

An OpN that does (Fin n -> A) -> A would not help with funext. OpN n A = Vec A n -> A would. Will that remove all uses of funext? I don't know. It would certainly remove some of them.

Working with Fin has been fine for me - once I moved away from subst. subst is a design smell. Luckily, and often with the help of others in the Agda community (the Zulip chat is super useful), I've been able to remove all such uses.

Regarding relational structures: I think it would be worthwhile to have multiple areas in agda-algebras. agda-categories has Categories.Enriched where things are redone but in an enriched way. We've been pondering a separate WithK as well. My feeling would be to have a single multi-pronged library, but with coherent design choices. It makes sense to have different libraries for different meta-theories, even if they are all embedded in Agda.

Not model-theory per se, but [Wolfram Kahl's(https://www.cas.mcmaster.ca/~kahl/) RATH-Agda contains a lot of relevant material. agda-categories really only contains category theory. Sometimes there's a bit of overlap, but it doesn't even have a good definition of Lawvere theories... (I need to redo that).

For both relational structures and the usual ones, if you're going to go countable, it's worth exploring the standard library's n-ary support (that's just an introduction, there's more). See also the paper "Generic Level Polymorphic N-ary Functions" on G. Allais's publications page. Lots of good stuff here.

Thank you very much for all this useful information and for sharing your expertise. It and the links are a lot to process. I'll respond again later after digesting it. Thanks!

	--The type of operations
	Op : Type 𝓥 → Type 𝓤 → Type(𝓤 ⊔ 𝓥)
	Op I A = (I → A) → A