Amélia

Making an opaque copy of (an `eta-equality` version of) the record + constructor + projections, sadly, doesn't quite work — though it was the first translation @TOTBWF and I both...

The translation does not rely on the unit type being a definitional singleton, since the `eta` token that's included in the translated records computes away. The translation also only exists...

@TOTBWF can you add a mention of the Borceux page to the index? Under the HoTT and Elephant pages

> Could you fix the problem by using `hooray : {A : Set} → A → Term → TC ⊤` instead of `hooray : PostponedTerm → Term → TC ⊤`?...

This is an intermediate step to reflecting abstract syntax, which avoids many of the complications (like reflecting: record constructor/update syntax, ambiguous names, etc), by... essentially being a bodge. The idea...

Is it already possible to extend a locally defined module by putting it inside an anonymous module, as in ```agda module _ where module X where postulate A : Set...

I'll see if I can come up with a way to trigger each (e.g. by modifying the strings locally).

Here's one that hits `cannotCreate` in general ("Can not transport with type family: P"). I suspect that the GenericDocErrors can not be hit since they're "guarded" by the `trFillTel`, but...

> Cubical Agda uses irrelevance in some way, right? Yes, but not in an essential way. We use it in the definition of `Partial`/`PartialP`: `Partial φ A` is defined to...

That's probably worse than just keeping `Total-hom`, but maybe it should be called `∫Hom` and have an anonymous constructor (and probably be an eta-equality type?). Maybe the fields could be...