From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Tue, 24 Apr 2018 19:10:42 -0700 (PDT)
From: Jeff Olson <jeff.d...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <48ab0dfe-f1e6-4447-9d6a-bbd678eb67c1@googlegroups.com>
In-Reply-To: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com>
References: <7f3c276a-2d81-4235-8f2a-c4d82ea4f827@googlegroups.com>
Subject: Re: Univalence from scratch
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_25402_177166391.1524622242345"

------=_Part_25402_177166391.1524622242345
Content-Type: multipart/alternative; 
	boundary="----=_Part_25403_1053751934.1524622242345"

------=_Part_25403_1053751934.1524622242345
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit

I posted a version written in Idris here 
(https://github.com/jdolson/univalence-from-scratch) if anyone is curious. 
-Jeff

------=_Part_25403_1053751934.1524622242345
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: 7bit

<div dir="ltr">I posted a version written in Idris here (https://github.com/jdolson/univalence-from-scratch) if anyone is curious. -Jeff</div>
------=_Part_25403_1053751934.1524622242345--

------=_Part_25402_177166391.1524622242345--