search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

some facts about smash product #464

Closed ecavallo closed 5 years ago

ecavallo commented 5 years ago

Don't think I have anything feasible left to do on this branch.

I moved cool.pointed => basics.pointed also.

ecavallo commented 5 years ago

Now that I'm thinking about it, how does this sound:

  1. Move the definitions of ptype, pmap, p→, and pequiv from basics.pointed to prelude.pointed, so that definitions in data can depend on them.
  2. Move the definition of smash from cool.smash to data.smash (this depends on ptype).
  3. Create pointed/, then move a. everything else in basics.pointed to pointed.bool and pointed.loops, b. everything else in cool.smash to pointed.smash.
favonia commented 5 years ago

Essentially you are growing the core library. :smiley_cat: