[Agda] Record types are not allowed in mutual blocks

[Thorsten Altenkirch]

Hi Nisse,

>> Is there any way to switch off this check which stops me from doing
>> this?
> 
> I'm sure there is, but we want to avoid infinite η-expansion.

Just to give some background. We are trying to define weak omega categories as a first step towards weak omega groupoids and eventually higher dimensional models of Type Theory.

This turns out to be quite tricky or maybe we haven't yet come up with the right way of doing this.

Basically a weak omega category is a category whose homsets are weak omega cats again, composition is a functor from 
hom b c x hom a c => hom a b and actually identity is a functor 1 => hom a a where 1 is the terminal weak omega cat and x is the product of weak omega cats. Weak means that all the equations are expressed as natural isomorphisms between functors. Coherence means that any diagram which only consists out of these natural isos should commute.

Our approach is to define at the same time weak omega categories, functors between them, products of weak omega categories and the associated morphisms and natural transformations exploiting coinductive definitions. It is not only convenient to use records for structures like weak omega cats but also not having eta is quite a pain.

I think your condition has to be justified otherwise it would be partial anyway. 

For the moment it would be an advantage if it would be at least possible to disable the check.

I am not sure this is enough for this project - it seems that a more structural approach to equality would be quite helpful too.

Cheers,
Thorsten

> Perhaps we
> can avoid this by requiring that any cycle from a record type to itself
> is "guarded" by a data type (or ∞).
> 
> -- 
> /NAD
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda