-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
73 lines (50 loc) · 2.79 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
<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
<title>Higher Types — Home</title>
<link rel="stylesheet" type="text/css" href="./css/default.css" />
<link rel="stylesheet" type="text/css" href="./css/agda.css" />
<script>
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
(i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
})(window,document,'script','//www.google-analytics.com/analytics.js','ga');
ga('create', 'UA-74182143-1', 'auto');
ga('send', 'pageview');
</script>
</head>
<body>
<div id="header">
<div id="logo">
<a href="./index.html">Higher Types</a>
</div>
<div id="navigation">
<a href="./index.html">Home</a>
<a href="./about.html">About</a>
<a href="./contact.html">Contact</a>
<a href="./archive.html">Archive</a>
</div>
</div>
<div id="content">
<h1>Home</h1>
<p>Welcome to my blog!</p>
<div class="post-teaser">
<h2><a href="./posts/CwF.html">Categories with Families...in Agda!</a> — February 9, 2016</h2>
<p><div class="post">
Posted on February 9, 2016
by <a href="mailto:[email protected]">Matthew Weaver</a>
</div>
<p>Here is a definition of categories with families I implemented in Agda. I wrote this using a neat category theory library.<a href="#fn1" class="footnoteRef" id="fnref1"><sup>1</sup></a> A category with families (CwF) is a categorical model of dependent type theory introduced by Peter Dybjer.<a href="#fn2" class="footnoteRef" id="fnref2"><sup>2</sup></a> Recently, they’ve been used with much success to model type theories with higher dimensional structures, such as higher dimensional equality,<a href="#fn3" class="footnoteRef" id="fnref3"><sup>3</sup></a> an internalized computational interpretation of parametricity,<a href="#fn4" class="footnoteRef" id="fnref4"><sup>4</sup></a> and a primative notion of names.<a href="#fn5" class="footnoteRef" id="fnref5"><sup>5</sup></a></p>
</p>
<p><a href="./posts/CwF.html">Read more...</a></p>
</div>
<p>For more posts, check out the <a href="./archive.html">archive</a>.</p>
</div>
<div id="footer">
Site proudly generated by
<a href="http://jaspervdj.be/hakyll">Hakyll</a>
</div>
</body>
</html>