amelia
/
cubical
1
0
Fork 0
Code Issues 0 Pull Requests 0 Projects 0 Releases 0 Wiki Activity

Commit Graph

  • a80e724 (HEAD -> master) Check in more experiments I had locally by Amélia Liao 2021-10-07 16:24:49 -0300
  • ec01798 Major refactoring of intro.tt + π₁(S¹) by Amélia Liao 2021-06-14 17:13:52 -0300
  • e52995a Remove `(φ = i0) as p` syntax + clean up proof of univalence + formalise theorems 4.7.6, 4.7.7, 7.2.2 by Amélia Liao 2021-05-05 16:46:32 -0300
  • 37506ac Rearrange definitions in example code by Amélia Liao 2021-05-04 00:35:58 -0300
  • bba4c57 Some fixes to prove univalence by Amélia Liao 2021-05-04 00:35:11 -0300
  • 79f6bfa optimise transport in Glue using gcomp by Amélia Liao 2021-04-17 19:03:44 -0300
  • d9ac1c4 Fixes to composition of HITs by Amélia Liao 2021-04-14 11:41:03 -0300
  • e9691c4 Small tweaks to some builtins by Amélia Liao 2021-04-10 03:04:50 -0300
  • b65c2e7 Use GluedVl to improve printing of isEquiv by Amélia Liao 2021-04-06 21:31:55 -0300
  • 81ed8ae Add strict equality by Amélia Liao 2021-04-06 08:36:48 -0300
  • 9421518 implement composition for HITs by Amélia Liao 2021-03-31 18:55:35 -0300
  • 8a27ec2 Fix recursive local lets by Amélia Liao 2021-03-14 01:58:13 -0300
  • fd5d162 Allow computing past 'case' by Amélia Liao 2021-03-13 13:10:53 -0300
  • 35a3247 Consolidate definitions of wired-in names by Amélia Liao 2021-03-10 08:39:02 -0300
  • 2ff359d (feature/web) initial work on web ughr by Abigail Magalhães 2021-03-18 10:33:08 -0300
  • de5e1e3 (feature/hits) Fix recursive local lets by Abigail Magalhães 2021-03-14 01:58:13 -0300
  • f3dc148 misc fixes + proof that T² = S¹×S¹ by Abigail Magalhães 2021-03-13 13:10:53 -0300
  • 9365797 put all the disgusting magic variables in one place by Abigail Magalhães 2021-03-10 08:39:02 -0300
  • f745f73 fix composition for the universe by Amélia Liao 2021-03-10 01:25:13 -0300
  • 7bcbc28 fix composition for the universe by Abigail Magalhães 2021-03-10 01:25:13 -0300
  • b4cf411 more pain and suffering by Amélia Liao 2021-03-08 02:56:21 -0300
  • f695f9b more pain and suffering by Abigail Magalhães 2021-03-08 02:56:21 -0300
  • d5c221c some initial work on HITs by Amélia Liao 2021-03-06 23:36:47 -0300
  • fb87b16 some initial work on HITs by Abigail Magalhães 2021-03-06 23:36:47 -0300
  • 9c37655 some fixes to inductive types by Amélia Liao 2021-03-06 18:20:12 -0300
  • 15cfd9a some fixes to inductive types by Abigail Magalhães 2021-03-06 18:20:12 -0300
  • 6827a88 Implement proper inductive types by Amélia Liao 2021-03-06 02:47:35 -0300
  • b423841 Implement proper inductive types by Abigail Magalhães 2021-03-06 02:47:35 -0300
  • 7aa7a3f Add where clauses by Amélia Liao 2021-03-04 18:39:01 -0300
  • 9761361 Add where clauses by Abigail Magalhães 2021-03-04 18:39:01 -0300
  • 6d065cd Use glued evaluation to get shorter normal forms by Amélia Liao 2021-03-04 16:28:17 -0300
  • 7d3ed1c Use glued evaluation to get shorter normal forms by Abigail Magalhães 2021-03-04 16:28:17 -0300
  • 6d82ecd Fix composition for pairs by Amélia Liao 2021-03-03 17:55:52 -0300
  • 28e1867 Fix composition for pairs by Abigail Magalhães 2021-03-03 17:55:52 -0300
  • 0a68d57 include proof of strong funext by Amélia Liao 2021-03-03 00:43:34 -0300
  • afa9440 include proof of strong funext by Abigail Magalhães 2021-03-03 00:43:34 -0300
  • e521e7f Report unsolved metas & composition for the universe by Amélia Liao 2021-03-02 23:18:29 -0300
  • 2fdd17b Report unsolved metas & composition for the universe by Abigail Magalhães 2021-03-02 23:18:29 -0300
  • 5797072 Composition for the universe by Amélia Liao 2021-03-01 10:43:31 -0300
  • f7d8fa0 Composition for the universe by Abigail Magalhães 2021-03-01 10:43:31 -0300
  • 8937bc1 Remove special handling of neutral I-eliminations in unifier by Amélia Liao 2021-03-01 09:50:31 -0300
  • 27e9be1 Remove special handling of neutral I-eliminations in unifier by Abigail Magalhães 2021-03-01 09:50:31 -0300
  • 8079ef8 built-in bools (to be removed later) by Amélia Liao 2021-03-01 03:06:58 -0300
  • 46b4703 built-in bools (to be removed later) by Abigail Magalhães 2021-03-01 03:06:58 -0300
  • 4ad8730 Document glueing + univalence by Amélia Liao 2021-02-27 23:18:09 -0300
  • ce9e987 Document glueing + univalence by Abigail Magalhães 2021-02-27 23:18:09 -0300
  • e09d035 Add let definitions by Amélia Liao 2021-02-27 23:18:00 -0300
  • d261ccc Add let definitions by Abigail Magalhães 2021-02-27 23:18:00 -0300
  • 1e6e17c Implement Glueing by Amélia Liao 2021-02-27 19:10:59 -0300
  • 5c50e1f Implement Glueing by Abigail Magalhães 2021-02-27 19:10:59 -0300
  • eb83b77 Implement cubical subtypes and composition by Amélia Liao 2021-02-27 04:17:15 -0300
  • 2d0b003 Implement cubical subtypes and composition by Abigail Magalhães 2021-02-27 04:17:15 -0300
  • 30b2984 Implement partial elements and systems by Amélia Liao 2021-02-26 23:17:32 -0300
  • 29285d0 Implement partial elements and systems by Abigail Magalhães 2021-02-26 23:17:32 -0300
  • 134c24c Implement dependent paths (PathP's) by Amélia Liao 2021-02-26 12:12:08 -0300
  • 79cb947 Implement dependent paths (PathP's) by Abigail Magalhães 2021-02-26 12:12:08 -0300
  • 818b816 Wired in definitions for the interval algebra by Amélia Liao 2021-02-26 01:29:11 -0300
  • a1a8a96 Wired in definitions for the interval algebra by Abigail Magalhães 2021-02-26 01:29:11 -0300
  • 9be5402 Polish up the type checker by Amélia Liao 2021-02-25 19:35:48 -0300
  • 92b50a4 Polish up the type checker by Abigail Magalhães 2021-02-25 19:35:48 -0300
  • c4a2fee Implement offside rule for toplevel statements by Amélia Liao 2021-02-25 15:34:36 -0300
  • 6ee7be2 Implement offside rule for toplevel statements by Abigail Magalhães 2021-02-25 15:34:36 -0300
  • b819f56 Definitional eta equality by Amélia Liao 2021-02-25 13:55:13 -0300
  • 954356f Definitional eta equality by Abigail Magalhães 2021-02-25 13:55:13 -0300
  • 1de859f Tweak the parser a bit by Amélia Liao 2021-02-25 04:32:01 -0300
  • b1e2e72 Tweak the parser a bit by Abigail Magalhães 2021-02-25 04:32:01 -0300
  • 6eae8f2 Implement MLTT elaborator w/ type inference by Amélia Liao 2021-02-25 02:47:36 -0300
  • fcd5428 Implement MLTT elaborator w/ type inference by Abigail Magalhães 2021-02-25 02:47:36 -0300
  • 6f0cef0 initial commit w/ lexer & parser by Amélia Liao 2021-02-24 03:18:43 -0300
  • bd3efa2 initial commit w/ lexer & parser by Abigail Magalhães 2021-02-24 03:18:43 -0300