[Agda] many ways to import the same thing from record

[mechvel at scico.botik.ru]

On 2020-06-08 23:15, mechvel at scico.botik.ru wrote:
> 
> [..]
> 

> This is an approach to define Class, SubClasss, SubSubClass ...
> where  SubClass has Class as an argument.
> 

An important correction of a typo:

    IsSubClass has Class as an argument.

--
SM