A word of caution [hca/H00F.lagda]

Agda uses its own type theory that is not HoTT.

Specifically the K-Rule is incompabtible with Homotopy Type Theory. Adding {-# OPTIONS --with-K #-} disables it.

Cubical Agda impelemts a different type theory that pairs more nicely with HoTT.