transporting ≃ and =

Stream: general

[Timo Carlin-Burns]

Has there been any work done on automatically generating congruence principles for inductive types like the following?

def Fin.equivCongr : n = m → Fin n ≃ Fin m := sorry
def Vector.equivCongr : T ≃ U → n = m → Vec T n ≃ Vec U m := sorry
def Sigma.equivCongr (e : α ≃ α') : (∀ a a', e a = a' → β a ≃ β' a') → Sigma β ≃ Sigma β' := sorry

(Notice that the appropriate hypotheses get a bit more complicated as dependent types get involved)

I've been playing around with this, and in the case of inductive families like Vector, proving the congruence principles require induction on the index type (e.g. Nat). This induction would only get more complicated if you had e.g. a family indexed by values in another family, so I think it might take some insight to design a modular procedure for generating these.

[Adam Topaz]

I don't know of any work toward this, but I think it's a worthwhile metaprogramming challenge. For one, you have to decide when to use equality and when to use an equivalence (maybe even go further, and ask for an equivalence of categories as a parameter when appropriate?!).

[Kyle Miller]

I was thinking about this a couple months ago.

Ideally, there would be something that could figure out whether the maps on type parameters have to be covariant, contravariant, an equivalence, or an equality, and then produce the functor, rather than just an equivalence.

[Kyle Miller]

For example, you could generate this:

def Vector.map : T -> U → n = m → Vec T n -> Vec U m := sorry

[Kyle Miller]

The Sigma example is more interesting, and what I remember is that can deduce that e has to be an equivalence if you want to write it as

def Sigma.map (e : α ≃ α') : (∀ a, β a -> β' (e a)) → Sigma β -> Sigma β' := sorry

(I'm not sure what factoring out that equality e a = a' could do. It seems like it could potentially be useful to make it easier to apply, but usually it's not necessary.)

[Timo Carlin-Burns]

My thinking was that e a = a' might be the way to express "a is equivalent to a'" given e : α ≃ α and it seemed simplest to have the consistent "shape" for congruence hypotheses "if the inputs are equivalent, the outputs are equivalent"

[Kyle Miller]

I don't remember which type needed that to be an equiv, bot docs#Sigma.map shows equivalence isn't necessary here.

Maybe it was just for the purpose of putting e to the left side, which could be necessary for some applications. (I was imagining using these auto-generated congruences for implementing a simp for equivalences.)