toothbrush/agda-gp — comment on commit dc0a49aa8de7bb4f6cc18e652919fe7367056cf7
File: Conversion.agda line 55
By jpcooper:

This is just a proof that A has a type representation in the spine universe, and it is useful in the definition of the following fields.