-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
108 lines (108 loc) · 5.62 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
<html>
<head>
<meta charset="utf-8" />
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
<meta name="description" content="" />
<meta name="author" content="Maxim Sokhatsky" />
<link href="https://fonts.googleapis.com/css?family=Montserrat:900" rel="stylesheet">
<title>CUBICAL</title>
<link rel="stylesheet" href="https://5ht.co/blank.css" />
</head>
<body>
<nav>
<a href='https://groupoid.space/'>GROUPOID</a>
</nav>
<header>
<h1>CUBICAL</h1>
</header>
<aside>
<article>
<section>
<h3>SYNOPSIS</h3>
<div>This page contains Groupoid Infinity cubical base library
for different cubical type checkers and proof assistants.<br><br></div>
<div>2016—2019 © <a href="https://5ht.co/license.htm">ISC</a></div>
</section>
<section>
<h3>NOTES</h3>
<div>There are several flavors of cubical type theory.
One takes its roots from <a href="http://www.cse.chalmers.se/~coquand/mod1.pdf">BCH</a>
paper that was formally given in <a href="https://arxiv.org/pdf/1611.02108.pdf">CCHM</a>
and implemented in Haskell as <a href="https://github.com/mortberg/cubicaltt">cubicaltt</a>.
The second lineage is cartesian cubical type theory that was presented
in <a href="https://guillaumebrunerie.github.io/pdf/cart-cube.pdf">ABCFHL</a>
and <a href="https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf">AFH</a> papers,
and implemented as <a href="https://github.com/RedPRL/redtt">redtt</a>,
<a href="https://github.com/mortberg/yacctt">yacctt</a>, and
<a href="https://github.com/JetBrains/Arend">Arend</a>.
</div>
</section>
</article>
</aside>
<main>
<section>
<p>Groupoid Infinity:</p>
</section>
<section>
<a name=cubicaltt></a>
<h3><a href="https://groupoid.space/mltt/types">cubicaltt</a></h3>
<p> The <b>cubicaltt</b> is a cubical type checker by Anders Mörtberg that supports path interval,
its connections, homogeneous path compositions, higher inductive types,
gluening of types and values. Recursive HITs have complete support only in <b>hcomp</b> version.
</p>
<ul>
<li><a href="https://github.com/groupoid/cubical">groupoid/cubical</a> — Groupoid Infinity cubical base library for cubicaltt type checker.</li>
<li><a href="https://github.com/groupoid/hopf">groupoid/hopf</a> — Hopf Fibrations for cubicaltt type checker.</li>
<li><a href="https://github.com/groupoid/infinity">groupoid/infinity</a> — cubical syntax.</li>
<li><a href="https://github.com/mortberg/cubicaltt">mortberg/cubicaltt</a> — cubical type checker (Haskell) with recursive HITs.</li>
<li><a href="https://github.com/mortberg/yacctt">mortberg/yacctt</a> — cartesian cubical type checker (Haskell).</li>
</ul>
</section>
<section>
<a name=Arend></a>
<h3><a href="https://github.com/JetBrains/arend">Arend</a></h3>
<p> <b>Arend</b> is a cartesian cubical type checker by JetBrains that supports HITs, extensible records,
type classes, implicit variables. It also contains Agda-style reasoning library.
</p>
<ul><li><a href="https://github.com/groupoid/arend">groupoid/arend</a> — Groupoid Infinity cubical base library for Arend.</li>
<li><a href="https://github.com/JetBrains/Arend">JetBrains/Arend</a> — Arend proof assistant.</li>
</ul>
</section>
<section>
<a name=Lean></a>
<h3><a href="https://github.com/groupoid/lean">Lean</a></h3>
<p>Ground Zero is a cubical model and cubical base library embedded into <b>Lean</b>.</p>
<ul><li><a href="https://github.com/groupoid/lean">groupoid/lean</a> — Ground Zero cubical base library for Lean 3 proof assistant.</li>
<li><a href="https://github.com/gebner/hott3">gebner/hott3</a> — HoTT library for Lean 3.</li>
<li><a href="https://github.com/leanprover/lean">leanprover/lean</a> — Lean 3.4.1 (C++).</li>
</ul>
</section>
<section>
<a name=Agda></a>
<h3><a href="https://github.com/groupoid/agda">Agda</a></h3>
<p>This is a base library for <b>Agda</b> in cubical mode.</p>
<ul><li><a href="https://github.com/groupoid/agda">groupoid/agda</a> — Groupoid Infinity cubical base library for Agda.</li>
<li><a href="https://github.com/agda/agda">agda/agda</a> — Agda proof assistant (Haskell).</li>
</ul>
</section>
<section>
<p>Other Cubical Type Systems and Libraries:</p>
</section>
<section>
<a name=Red></a>
<h3><a href="https://github.com/RedPRL">RedPRL</a></h3>
<p> The <b>redtt</b> is a cartesian cubical type checker
that take its roots from <a href="https://github.com/RedPRL/sml-redprl">RedPRL</a>
and <a href="https://github.com/jonsterling/jonprl">JonPRL<a>.
</p>
<ul><li><a href="https://github.com/RedPRL/sml-redprl">RedPRL/RedPRL</a> — PRL-family proof assistant (Standard ML).</li>
<li><a href="https://github.com/RedPRL/redtt">RedPRL/redtt</a> — cartesian cubical type checker (OCaml).</li>
</ul>
<br>
<p></p>
</section>
</main>
<footer>CTTへの<span class="heart"> ❤ </span>をもって作られた</footer>
</body>
</html>