Jarl G. Taxerås Flaten comments

Repositories
Issues
Comments

Results 3 comments of


                                            Jarl G. Taxerås Flaten

Unify `BAut X` with `Type_ O`?

If we define `BAut X` to be `{ Z : Type & merely (Z X) }` then proving connectedness requires univalence, so any statement about `BAut X` as an oo-group...

Reversible coercions (+ canonical structures and typeclasses)

Indeed! Does this solve #1530?

build Setup.hs with local compiler when cross-compiling

@sheyll any progress lately? I would be willing to test it out if you have something working. I want to cross-compile a cabal sandbox on a x86_64 server for use...