<?xml version="1.0" encoding="utf-8"?>
<rss version="2.0"
	xmlns:content="http://purl.org/rss/1.0/modules/content/"
	xmlns:wfw="http://wellformedweb.org/CommentAPI/"
	xmlns:dc="http://purl.org/dc/elements/1.1/"
	xmlns:atom="http://www.w3.org/2005/Atom"
	xmlns:sy="http://purl.org/rss/1.0/modules/syndication/"
	xmlns:slash="http://purl.org/rss/1.0/modules/slash/"
	>

<channel>
	<title>Epilogue &#187; Observational Type Theory</title>
	<atom:link href="http://www.e-pig.org/epilogue/?feed=rss2&#038;cat=3" rel="self" type="application/rss+xml" />
	<link>http://www.e-pig.org/epilogue</link>
	<description>for Epigram</description>
	<lastBuildDate>Tue, 03 Jan 2012 13:02:31 +0000</lastBuildDate>
	<generator>http://wordpress.org/?v=2.8.4</generator>
	<language>en</language>
	<sy:updatePeriod>hourly</sy:updatePeriod>
	<sy:updateFrequency>1</sy:updateFrequency>
			<item>
		<title>Hier Soir, an OTT Hierarchy</title>
		<link>http://www.e-pig.org/epilogue/?p=1098</link>
		<comments>http://www.e-pig.org/epilogue/?p=1098#comments</comments>
		<pubDate>Sat, 12 Nov 2011 23:18:53 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>
		<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=1098</guid>
		<description><![CDATA[I&#8217;m still waiting for my computer to typecheck this file, which I concocted yesterday evening. I&#8217;m told by someone with a better computer (thanks, Darin) that it does typecheck, and moreover, satisfy the termination checker. It relies unexcitingly on the size-change principle and is easily rendered entirely structural.
What I&#8217;ve managed to do (at last!) is [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=1098</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
		<item>
		<title>Coinduction, observationally</title>
		<link>http://www.e-pig.org/epilogue/?p=418</link>
		<comments>http://www.e-pig.org/epilogue/?p=418#comments</comments>
		<pubDate>Mon, 22 Mar 2010 17:51:27 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=418</guid>
		<description><![CDATA[I thought I might report a bit about what I&#8217;ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.
What I&#8217;ve got is an Agda universe with inductive and coinductive Petersson-Synek [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=418</wfw:commentRss>
		<slash:comments>5</slash:comments>
		</item>
		<item>
		<title>W-types: good news and bad news</title>
		<link>http://www.e-pig.org/epilogue/?p=324</link>
		<comments>http://www.e-pig.org/epilogue/?p=324#comments</comments>
		<pubDate>Sun, 07 Mar 2010 21:50:45 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>
		<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=324</guid>
		<description><![CDATA[I thought I&#8217;d just collect together some disparate observations about W-types, and their use in encoding other recursive datatypes. My motivation, bluntly, is to point out the inevitable unsuitability of W-types as the basis for recursive datatypes in an implementation of decidable type theories. I don&#8217;t want to downplay the conceptual importance of W-types as [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=324</wfw:commentRss>
		<slash:comments>5</slash:comments>
		</item>
		<item>
		<title>Quotients</title>
		<link>http://www.e-pig.org/epilogue/?p=319</link>
		<comments>http://www.e-pig.org/epilogue/?p=319#comments</comments>
		<pubDate>Mon, 08 Feb 2010 14:02:54 +0000</pubDate>
		<dc:creator>Conor</dc:creator>
				<category><![CDATA[General]]></category>
		<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=319</guid>
		<description><![CDATA[I&#8217;ve had an enquiry for more details on quotients in the new Epigram setup, so I&#8217;ll take that as a cue to blog a bit.
First, I&#8217;d better sketch some basics about propositions and equality. It&#8217;s the novel treatment of these things which lets us handle quotients in (hopefully) a neater way than has been possible [...]]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=319</wfw:commentRss>
		<slash:comments>1</slash:comments>
		</item>
		<item>
		<title>OTT by reflecting telescopes</title>
		<link>http://www.e-pig.org/epilogue/?p=43</link>
		<comments>http://www.e-pig.org/epilogue/?p=43#comments</comments>
		<pubDate>Mon, 16 May 2005 15:53:59 +0000</pubDate>
		<dc:creator>txa</dc:creator>
				<category><![CDATA[Observational Type Theory]]></category>

		<guid isPermaLink="false">http://www.e-pig.org/epilogue/?p=43</guid>
		<description><![CDATA[Starting point: TT with some proper dependency, e.g. 
	  b : Bool
	  &#8212;&#8212;&#8212;&#8212;&#8211;
	  T b : *
	  T false = Null
	  T true  = One
we assume at least Pi, Sigma, Empty, Null, One, Bool. We also use Prop ]]></description>
		<wfw:commentRss>http://www.e-pig.org/epilogue/?feed=rss2&amp;p=43</wfw:commentRss>
		<slash:comments>0</slash:comments>
		</item>
	</channel>
</rss>
