michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Added support for citations.

Browse source
This commit is contained in:
Wen Kokke 2020-10-26 17:05:04 +01:00
parent e33b5fc952
commit 2c4bf84365
5 changed files with 747 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
bib/plfa.bib Normal file
View file

@ -0,0 +1,15 @@
@BOOK{plfa20.07,
author = {Philip Wadler and Wen Kokke and Jeremy G. Siek},
title = {Programming Language Foundations in {A}gda},
year = {2020},
month = jul,
url = {http://plfa.inf.ed.ac.uk/20.07/},
}
@BOOK{plfa19.08,
author = {Philip Wadler and Wen Kokke},
title = {Programming Language Foundations in {A}gda},
year = {2019},
month = aug,
url = {http://plfa.inf.ed.ac.uk/19.08/},
}

584
csl/iso690-author-date-en.csl Normal file
View file

@ -0,0 +1,584 @@
<?xml version="1.0" encoding="utf-8"?>
<style xmlns="http://purl.org/net/xbiblio/csl" class="in-text" version="1.0" demote-non-dropping-particle="never" default-locale="en-US">
<info>
<title>ISO-690 (author-date, English)</title>
<id>http://www.zotero.org/styles/iso690-author-date-en</id>
<link href="http://www.zotero.org/styles/iso690-author-date-en" rel="self"/>
<link href="https://forums.zotero.org/discussion/20342" rel="documentation"/>
<link href="http://www.iso.org/iso/catalogue_detail.htm?csnumber=43320" rel="documentation"/>
<author>
<name>Laure Mellifluo</name>
<email>laure.melli@gmail.com</email>
</author>
<author>
<name>Raphael Grolimund</name>
<email>raphael.grolimund@epfl.ch</email>
</author>
<author>
<name>Michel Hardegger</name>
<email>hardegger@gmail.com</email>
</author>
<category citation-format="author-date"/>
<category field="generic-base"/>
<summary>Style based on ISO 690:2010(E), v1.1</summary>
<updated>2016-12-28T18:29:48+00:00</updated>
<rights license="http://creativecommons.org/licenses/by-sa/3.0/">This work is licensed under a Creative Commons Attribution-ShareAlike 3.0 License</rights>
</info>
<locale>
<terms>
<term name="no date">[no date]</term>
<term name="in">in</term>
<term name="online">online</term>
<term name="accessed">accessed</term>
<term name="retrieved">Available</term>
<term name="from">from</term>
</terms>
</locale>
<macro name="editor">
<names variable="editor">
<name and="text" name-as-sort-order="all" sort-separator=", " delimiter=", " delimiter-precedes-last="never">
<name-part name="family" text-case="uppercase"/>
<name-part name="given"/>
</name>
<label prefix=" (" form="short" suffix=".)"/>
</names>
</macro>
<macro name="translator">
<names variable="translator">
<name and="text" name-as-sort-order="all" sort-separator=", " delimiter=", " delimiter-precedes-last="never">
<name-part name="family" text-case="uppercase"/>
<name-part name="given"/>
</name>
<label prefix=" (" form="short" suffix=".)"/>
</names>
</macro>
<macro name="responsability">
<names variable="author">
<name and="text" name-as-sort-order="all" sort-separator=", " delimiter=", " delimiter-precedes-last="never">
<name-part name="family" text-case="uppercase"/>
<name-part name="given"/>
</name>
<substitute>
<text macro="editor"/>
<text macro="translator"/>
<text macro="title"/>
</substitute>
</names>
<choose>
<if variable="author editor translator" match="any">
<text macro="year-date" prefix=", "/>
</if>
</choose>
</macro>
<macro name="author-citation">
<names variable="author">
<name form="short"/>
<substitute>
<names variable="editor"/>
<names variable="translator"/>
<text variable="title" font-style="italic"/>
</substitute>
</names>
</macro>
<macro name="container-author">
<names variable="container-author">
<name and="text" name-as-sort-order="all" sort-separator=", " delimiter=", " delimiter-precedes-last="never">
<name-part name="family" text-case="uppercase"/>
<name-part name="given"/>
</name>
</names>
</macro>
<macro name="container-responsability">
<choose>
<if variable="container-author">
<text macro="container-author"/>
</if>
<else-if variable="editor">
<text macro="editor"/>
</else-if>
<else>
<text macro="translator"/>
</else>
</choose>
</macro>
<macro name="year-date">
<choose>
<if variable="issued">
<date variable="issued">
<date-part name="year" form="long"/>
</date>
</if>
<else>
<text term="no date"/>
</else>
</choose>
</macro>
<macro name="title">
<choose>
<if type="book thesis map motion_picture song manuscript" match="any">
<choose>
<if variable="author editor translator" match="any">
<text variable="title" font-style="italic"/>
</if>
<else>
<text variable="title" font-style="italic" suffix=", "/>
<text macro="year-date" suffix=". "/>
</else>
</choose>
</if>
<else-if type="paper-conference speech chapter article-journal article-magazine article-newspaper entry entry-dictionary entry-encyclopedia post-weblog post webpage broadcast" match="any">
<choose>
<if variable="author editor translator" match="any">
<text variable="title" suffix=". "/>
</if>
<else>
<text variable="title" suffix=", "/>
<text macro="year-date" suffix=". "/>
</else>
</choose>
<choose>
<if type="chapter paper-conference" match="any">
<text term="in" text-case="capitalize-first" suffix=": "/>
</if>
</choose>
<choose>
<if variable="container-author">
<text macro="container-responsability"/>
<choose>
<if variable="container-title event" match="any">
<text value=", "/>
</if>
</choose>
</if>
</choose>
<choose>
<if variable="container-title">
<text variable="container-title" font-style="italic"/>
</if>
<else>
<text variable="event" font-style="italic"/>
</else>
</choose>
</else-if>
<else-if type="report">
<choose>
<if variable="author editor translator" match="any">
<text variable="number" suffix=": "/>
<text variable="title" font-style="italic"/>
</if>
<else>
<text variable="number" suffix=": "/>
<text variable="title" font-style="italic" suffix=", "/>
<text macro="year-date" suffix=". "/>
</else>
</choose>
</else-if>
<else-if type="patent">
<choose>
<if variable="author editor translator" match="any">
<text variable="title"/>
</if>
<else>
<text variable="title" suffix=", "/>
<text macro="year-date" suffix=". "/>
</else>
</choose>
</else-if>
<else>
<choose>
<if variable="author editor translator" match="any">
<text variable="title" font-style="italic"/>
</if>
<else>
<text variable="title" font-style="italic" suffix=", "/>
<text macro="year-date" suffix=". "/>
</else>
</choose>
</else>
</choose>
<choose>
<if variable="URL">
<text term="online" prefix=" [" suffix="]"/>
</if>
</choose>
</macro>
<macro name="number">
<text variable="number"/>
</macro>
<macro name="medium">
<text variable="medium" prefix=" [" suffix="]"/>
</macro>
<macro name="genre">
<choose>
<if type="map">
<choose>
<if variable="genre">
<text variable="genre" prefix="[" suffix="]"/>
</if>
<else>
<text value="map" prefix="[" suffix="]"/>
</else>
</choose>
</if>
<else>
<text variable="genre"/>
</else>
</choose>
</macro>
<macro name="date">
<choose>
<if variable="issued">
<date variable="issued">
<date-part name="day" suffix=" "/>
<date-part name="month" suffix=" "/>
<date-part name="year"/>
</date>
</if>
</choose>
</macro>
<macro name="edition">
<text variable="edition" form="long"/>
</macro>
<macro name="publisher-group">
<group delimiter=": ">
<text variable="publisher-place"/>
<text variable="publisher"/>
</group>
</macro>
<macro name="issue">
<group delimiter=", ">
<text variable="volume" prefix="Vol.&#160;"/>
<choose>
<if variable="volume">
<text variable="issue" prefix="no.&#160;"/>
<text variable="page" prefix="p.&#160;"/>
</if>
<else-if variable="issue">
<text variable="issue" prefix="No.&#160;"/>
<text variable="page" prefix="p.&#160;"/>
</else-if>
<else>
<text variable="page" prefix="P.&#160;"/>
</else>
</choose>
</group>
</macro>
<macro name="accessed">
<choose>
<if variable="URL">
<group prefix=" [" suffix="]">
<text term="accessed" text-case="capitalize-first"/>
<date variable="accessed">
<date-part name="day" prefix="&#160;"/>
<date-part name="month" prefix="&#160;"/>
<date-part name="year" prefix="&#160;"/>
</date>
</group>
</if>
</choose>
</macro>
<macro name="collection">
<group delimiter=", ">
<text variable="collection-title"/>
<text variable="collection-number"/>
</group>
</macro>
<macro name="page">
<choose>
<if type="book thesis manuscript" match="any">
<text variable="number-of-pages" suffix="&#160;p"/>
</if>
<else-if type="chapter paper-conference article-newspaper" match="any">
<text variable="page" prefix="p.&#160;"/>
</else-if>
<else-if type="report patent" match="any">
<text variable="page" suffix="&#160;p"/>
</else-if>
</choose>
</macro>
<macro name="isbn">
<text variable="ISBN" prefix="ISBN&#160;"/>
</macro>
<macro name="doi">
<text variable="DOI" prefix="DOI&#160;"/>
</macro>
<macro name="url">
<choose>
<if variable="URL">
<group>
<text term="retrieved" suffix=" " text-case="capitalize-first"/>
<text term="from" suffix=": "/>
<text variable="URL"/>
</group>
</if>
</choose>
</macro>
<macro name="archive">
<group delimiter=":&#160;">
<text variable="archive"/>
<text macro="archive_location"/>
</group>
</macro>
<macro name="archive_location">
<choose>
<if variable="archive_location">
<text variable="archive_location"/>
</if>
<else>
<text variable="call-number"/>
</else>
</choose>
</macro>
<macro name="abstract">
<text variable="abstract"/>
</macro>
<macro name="note">
<text variable="note"/>
</macro>
<citation disambiguate-add-year-suffix="true" disambiguate-add-names="true" disambiguate-add-givenname="true" collapse="year" year-suffix-delimiter=", " after-collapse-delimiter="; ">
<layout prefix="(" suffix=")" delimiter="; ">
<group delimiter=", ">
<group delimiter=" ">
<text macro="author-citation"/>
<text macro="year-date"/>
</group>
<group>
<label variable="locator" suffix=".&#160;" form="short" strip-periods="true"/>
<text variable="locator"/>
</group>
</group>
</layout>
</citation>
<bibliography>
<sort>
<key macro="responsability"/>
<key macro="year-date"/>
</sort>
<layout>
<choose>
<if type="book map" match="any">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="isbn" suffix=". "/>
<text macro="url"/>
</group>
</if>
<else-if type="article-journal article-magazine" match="any">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="edition" suffix=". "/>
<text macro="date" suffix=". "/>
<text macro="issue" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="doi" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="article-newspaper">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=", "/>
<text macro="date" suffix=". "/>
<text macro="page" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="chapter entry entry-dictionary entry-encyclopedia" match="any">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="page" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="isbn" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="speech">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="date" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="page" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="paper-conference">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="date" suffix=". "/>
<text macro="page" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="isbn" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="thesis">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="post-weblog post webpage" match="any">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="date" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="broadcast motion_picture song" match="any">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="medium" suffix=". "/>
<text macro="publisher-group" suffix=", "/>
<text macro="date" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="isbn" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="report">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="manuscript">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="genre" suffix=". "/>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else-if type="patent">
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="number" suffix=". "/>
<text macro="date" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="url"/>
</group>
</else-if>
<else>
<group display="block">
<text macro="responsability" suffix=". "/>
<choose>
<if variable="author editor translator" match="any">
<text macro="title" suffix=". "/>
</if>
</choose>
<text macro="medium" suffix=". "/>
<text macro="genre" suffix=". "/>
<text macro="date" suffix=". "/>
<text macro="edition" suffix=". "/>
<text macro="publisher-group" suffix=". "/>
<text macro="number" suffix=". "/>
<text macro="accessed" suffix=". "/>
<text macro="collection" suffix=". "/>
<text macro="page" suffix=". "/>
<text macro="isbn" suffix=". "/>
<text macro="url"/>
</group>
</else>
</choose>
<group display="right-inline">
<text macro="archive"/>
</group>
<group display="right-inline">
<text macro="abstract"/>
</group>
<group display="right-inline">
<text macro="note"/>
</group>
</layout>
</bibliography>
</style>

51
hs/Main.hs
View file

@ -6,12 +6,14 @@ import Data.Functor ((<&>))
import qualified Data.Text as T
import Hakyll
import Hakyll.Web.Agda
import Hakyll.Web.Routes.Permalink
import Hakyll.Web.Template.Numeric
import Hakyll.Web.Template.Context.Metadata
import Hakyll.Web.Template.Context.Title
import Hakyll.Web.Sass
import Hakyll.Web.Routes.Permalink
import System.FilePath ((</>), takeDirectory)
import qualified Text.CSL as CSL
import qualified Text.CSL.Pandoc as CSL (processCites)
import Text.Pandoc (Pandoc(..), ReaderOptions(..), WriterOptions(..), Extension(..))
import qualified Text.Pandoc as Pandoc
import qualified Text.Pandoc.Filter as Pandoc (Filter(..), applyFilters)
@ -152,6 +154,9 @@ epubWriterOptions = siteWriterOptions
main :: IO ()
main = do
let cslFileName = "csl/iso690-author-date-en.csl"
let bibFileName = "bib/plfa.bib"
-- Build function to fix standard library URLs
fixStdlibLink <- mkFixStdlibLink agdaStdlibPath
@ -160,8 +165,12 @@ main = do
-- Build compiler for Markdown pages
let pageCompiler :: Compiler (Item String)
pageCompiler = getResourceBody
pageCompiler = do
csl <- load cslFileName
bib <- load bibFileName
getResourceBody
>>= readMarkdownWith siteReaderOptions
>>= processCites csl bib
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/page.html" siteSectionContext
@ -170,10 +179,14 @@ main = do
-- Build compiler for literate Agda pages
let pageWithAgdaCompiler :: CommandLineOptions -> Compiler (Item String)
pageWithAgdaCompiler opts = agdaCompilerWith opts
pageWithAgdaCompiler opts = do
csl <- load cslFileName
bib <- load bibFileName
agdaCompilerWith opts
>>= withItemBody (return . withUrls fixStdlibLink)
>>= withItemBody (return . withUrls fixLocalLink)
>>= readMarkdownWith siteReaderOptions
>>= processCites csl bib
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/page.html" siteSectionContext
@ -261,8 +274,12 @@ main = do
match "posts/*" $ do
route $ setExtension "html"
compile $ getResourceBody
compile $ do
csl <- load cslFileName
bib <- load bibFileName
getResourceBody
>>= readMarkdownWith siteReaderOptions
>>= processCites csl bib
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/post.html" postContext
@ -306,6 +323,10 @@ main = do
-- Compile templates
match "templates/*" $ compile templateBodyCompiler
-- Compile CSL and BibTeX files
match "csl/*.csl" $ compile cslCompiler
match "bib/*.bib" $ compile biblioCompiler
-- Copy resources
match "public/**" $ do
route idRoute
@ -345,16 +366,6 @@ main = do
-- Custom readers and writers
--------------------------------------------------------------------------------
-- | Read a CommonMark string using Pandoc, with the supplied options.
readCommonMarkWith :: ReaderOptions -- ^ Parser options
-> Item String -- ^ String to read
-> Compiler (Item Pandoc) -- ^ Resulting document
readCommonMarkWith ropt item =
case Pandoc.runPure $ traverse (Pandoc.readCommonMark ropt) (fmap T.pack item) of
Left err -> fail $
"Hakyll.Web.Pandoc.readPandocWith: parse failed: " ++ show err
Right item' -> return item'
-- | Read a Markdown string using Pandoc, with the supplied options.
readMarkdownWith :: ReaderOptions -- ^ Parser options
-> Item String -- ^ String to read
@ -365,6 +376,18 @@ readMarkdownWith ropt item =
"Hakyll.Web.Pandoc.readPandocWith: parse failed: " ++ show err
Right item' -> return item'
-- | Process citations in a Pandoc document.
processCites :: Item CSL -> Item Biblio -> Item Pandoc -> Compiler (Item Pandoc)
processCites csl bib item = do
-- Parse CSL file, if given
style <- unsafeCompiler $ CSL.readCSLFile Nothing . toFilePath . itemIdentifier $ csl
-- We need to know the citation keys, add then *before* actually parsing the
-- actual page. If we don't do this, pandoc won't even consider them
-- citations!
let Biblio refs = itemBody bib
withItemBody (return . CSL.processCites style refs) item
-- | Write a document as HTML using Pandoc, with the supplied options.
writeHTML5With :: WriterOptions -- ^ Writer options for pandoc
-> Item Pandoc -- ^ Document to write

1
src/pages/citing.md
View file

@ -25,7 +25,6 @@ permalink : /Citing/
}
```
## PLFA version 19.08
### Chicago

169
src/pages/notes.md
View file

@ -7,12 +7,16 @@ permalink: /Notes/
## To Do
Changes I would like to make to the book:
- Relations, exercise `o+o≡e` --> (recommended)
- Relations, exercise `≤-iff-<` --> `≤→<`, `<→≤`
- Relations, exercise `Bin-predicates` --> `Bin-predicate`
change canonical form of zero to be empty string, `<>`.
Change canonical form of zero to be empty string, `<>`.
Similar change to subsequent exercise.
## Citations
You can cite works by writing `@` followed by a citation key, e.g., `@plfa20.07`. For instance, the first release of PLFA was by @plfa19.08. See the [bibliography](#bibliography) section below for the bibliography. Citations and the bibliography are currently styled according to the ISO-690 standard.
## Downloading older versions
@ -105,24 +109,26 @@ Get evidence!
## Where to put Lists?
Three possible orders:
+ (a) As current
+ (b) Put Lists immediately after Induction.
1. As current
2. Put Lists immediately after Induction.
- requires moving composition & extensionality earlier
- requires moving parameterised modules earlier for monoids
- add material to relations:
lexical ordering, subtype ordering, All, Any, All-++ iff
- add material to isomorphism: All-++ isomorphism
- retain material on decidability of All, Any in Decidable
+ (c) Put Lists after Decidable
3. Put Lists after Decidable
- requires moving Any-decidable from Decidable to Lists
+ (d) As (b) but put parameterised modules in a separate chapter
4. As (2) but put parameterised modules in a separate chapter
Tradeoffs:
+ (b) Distribution of exercises near where material is taught
+ (b) Additional reinforcement for simple proofs by induction
+ (a,c) Can drop material if there is lack of time
+ (a,c) Earlier emphasis on induction over evidence
+ (c) More consistent structuring principle
+ (2) Distribution of exercises near where material is taught
+ (2) Additional reinforcement for simple proofs by induction
+ (1,3) Can drop material if there is lack of time
+ (1,3) Earlier emphasis on induction over evidence
+ (3) More consistent structuring principle
## Set up lists of exercises to do
@ -276,80 +282,79 @@ The following comments were collected on the Agda mailing list.
* Chalmer Take Home exam 2017
+ http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/TakeHomeExamTypes2017.pdf
## Syntax for lambda calculus
* ƛ \Gl-
* ∙ \.
## Adrian's comments from MeetUp
Adrian King
I think we've finally gone through the whole book now up through chapter Properties, and we've come up with just three places where we thought the book could have done a better job of preparing us for the exercises.
**Adrian King**:
Starting from the end of the book:
> I think we've finally gone through the whole book now up through chapter Properties, and we've come up with just three places where we thought the book could have done a better job of preparing us for the exercises.
>
> Starting from the end of the book:
>
> * Chapter Quantifiers, exercise Bin-isomorphism:
>
> In the `to∘from` case, we want to show that:
>
> ⟨ to (from x) , toCan {from x} ⟩ ≡ ⟨ x , canX ⟩
>
> I found myself wanting to use a general lemma like:
>
> ```
> exEq :
> ∀ {A : Set} {x y : A} {p : A → Set} {px : p x} {py : p y} →
> x ≡ y →
> px ≡ py →
> ⟨ x , px ⟩ ≡ ⟨ y , py ⟩
> exEq refl refl = refl
> ```
>
> which is in some sense true, but in Agda it doesn't typecheck, because Agda can't see that px's type and py's type are the same. My solution made explicit use of heterogeneous equality.
>
> I realize there are ways to solve this that don't explicitly use heterogeneous equality, but the surprise factor of the exercise might have been lower if heterogeneous equality had been mentioned by that point, perhaps in the Equality chapter.
>
> * Chapter Quantifiers, exercise ∀-×:
>
> I assume the intended solution looks something like:
>
> ```
> ∀-× : ∀ {B : Tri → Set} → ((x : Tri) → B x) ≃ (B aa × B bb × B cc)
> ∀-× = record {
> to = λ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ ;
> from = λ{ ⟨ baa , ⟨ bbb , bcc ⟩ ⟩ → λ{ aa → baa ; bb → bbb ; cc → bcc } } ;
> from∘to = λ f → extensionality λ{ aa → refl ; bb → refl ; cc → refl } ;
> to∘from = λ{ y → refl } }
> ```
>
> but it doesn't typecheck; in the extensionality presented earlier (in chapter Isomorphism), type B is not dependent on type A, but it needs to be here. Agda's error message is sufficiently baffling here that you might want to warn people that they need a dependent version of extensionality, something like:
>
> ```
> Extensionality : (a b : Level) → Set _
> Extensionality a b =
> {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
> (∀ x → f x ≡ g x) → f ≡ g
>
> postulate exten : ∀ {a b} → Extensionality a b
> ```
>
> * Chapter Relations, exercise Bin-predicates:
>
> I made use here of the inspect idiom, in Aaron Stump's variant, which is syntactically more convenient:
>
> ```
> keep : ∀ {ℓa} → {a : Set ℓa} → (x : a) → Σ a (λ y → y ≡ x)
> keep x = x , refl
> ```
>
> Pattern matching on keep m, where m is some complicated term, lets you keep around an equality between the original term and the pattern matched, which is often convenient, as in:
>
> ```
> roundTripTwice {x} onex with keep (from x)
> roundTripTwice {x} onex | zero , eq with oneIsMoreThanZero onex
> roundTripTwice {x} onex | zero , eq | 0<fromx rewrite sym eq =
> ⊥-elim (not0<0 0<fromx)
> roundTripTwice {x} onex | suc n , eq rewrite sym eq | toTwiceSuc {n} |
> cong x0_ (sym (roundTrip (one onex))) | sym eq = refl
> ```
>
* Chapter Quantifiers, exercise Bin-isomorphism:
In the to∘from case, we want to show that:
⟨ to (from x) , toCan {from x} ⟩ ≡ ⟨ x , canX ⟩
I found myself wanting to use a general lemma like:
```
exEq :
∀ {A : Set} {x y : A} {p : A → Set} {px : p x} {py : p y} →
x ≡ y →
px ≡ py →
⟨ x , px ⟩ ≡ ⟨ y , py ⟩
exEq refl refl = refl
```
which is in some sense true, but in Agda it doesn't typecheck, because Agda can't see that px's type and py's type are the same. My solution made explicit use of heterogeneous equality.
I realize there are ways to solve this that don't explicitly use heterogeneous equality, but the surprise factor of the exercise might have been lower if heterogeneous equality had been mentioned by that point, perhaps in the Equality chapter.
* Chapter Quantifiers, exercise ∀-×:
I assume the intended solution looks something like:
```
∀-× : ∀ {B : Tri → Set} → ((x : Tri) → B x) ≃ (B aa × B bb × B cc)
∀-× = record {
to = λ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ ;
from = λ{ ⟨ baa , ⟨ bbb , bcc ⟩ ⟩ → λ{ aa → baa ; bb → bbb ; cc → bcc } } ;
from∘to = λ f → extensionality λ{ aa → refl ; bb → refl ; cc → refl } ;
to∘from = λ{ y → refl } }
```
but it doesn't typecheck; in the extensionality presented earlier (in chapter Isomorphism), type B is not dependent on type A, but it needs to be here. Agda's error message is sufficiently baffling here that you might want to warn people that they need a dependent version of extensionality, something like:
```
Extensionality : (a b : Level) → Set _
Extensionality a b =
{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
(∀ x → f x ≡ g x) → f ≡ g
postulate
exten : ∀ {a b} → Extensionality a b
```
* Chapter Relations, exercise Bin-predicates:
I made use here of the inspect idiom, in Aaron Stump's variant, which is syntactically more convenient:
```
keep : ∀ {ℓa} → {a : Set ℓa} → (x : a) → Σ a (λ y → y ≡ x)
keep x = x , refl
```
Pattern matching on keep m, where m is some complicated term, lets you keep around an equality between the original term and the pattern matched, which is often convenient, as in:
```
roundTripTwice {x} onex with keep (from x)
roundTripTwice {x} onex | zero , eq with oneIsMoreThanZero onex
roundTripTwice {x} onex | zero , eq | 0<fromx rewrite sym eq =
⊥-elim (not0<0 0<fromx)
roundTripTwice {x} onex | suc n , eq rewrite sym eq | toTwiceSuc {n} |
cong x0_ (sym (roundTrip (one onex))) | sym eq = refl
```
## Bibliography