cubical

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

Commit Graph Mono Color

Commit Graph