Closed vikraman closed 3 years ago
There is already a definition in Pi+/Coxeter/Coxeter.agda, but we need another form, as a HIT.
Pi+/Coxeter/Coxeter.agda
There is already a definition in
Pi+/Coxeter/Coxeter.agda
, but we need another form, as a HIT.