search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
572 stars 76 forks source link

use retracts to prove n-types #106

Closed ecavallo closed 5 years ago

mortberg commented 5 years ago

Thanks! As discussed some of the results can probably be proved even more directly in the relevant special cases

3abc commented 5 years ago

Thanks! As discussed some of the results can probably be proved even more directly in the relevant special cases

I've found a direct proof. I have it ready in Agda and I will translate to cubicaltt.

mortberg commented 5 years ago

@3abc I think @ecavallo also had some more direct proofs. Please make some PRs! :-)

mortberg commented 5 years ago

I never spent much time optimizing the later maps in the definition as I was stuck in the middle, but it would be interesting to make progress of this now.

@3abc Did anything come out of your experiments of defining the eliminator for truncations? (https://github.com/agda/cubical/pull/74)

FYI: I'm going to be very busy with other things for almost a month now so I don't really have time to work much on this right now, but if you experiment more please keep me posted on your findings.

3abc commented 5 years ago

@3abc Did anything come out of your experiments of defining the eliminator for truncations? (agda/cubical#74)

Oh what I said above was meant to say I have direct proofs of the eliminators. I thought this PR is about the eliminators?

mortberg commented 5 years ago

@3abc Did anything come out of your experiments of defining the eliminator for truncations? (agda/cubical#74)

Oh what I said above was meant to say I have direct proofs of the eliminators. I thought this PR is about the eliminators?

Not exactly. Evan just simplified the proof that various types have specific hlevels, in particular there is now no need for the standard formulation of the univalence axiom.

3abc commented 5 years ago

Not exactly. Evan just simplified the proof that various types have specific hlevels, in particular there is now no need for the standard formulation of the univalence axiom.

Oh so it's about things like isGroupoid SET isTwoGroupoid GROUPOID. I see, great.