Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

marked missing material in the notes #1

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

marked missing material in the notes #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7282782
marked missing material in the notes (the identity and the constant f…
ohad Aug 6, 2013
af44018
minor typo
ohad Aug 6, 2013
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Exe1.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,6 +147,8 @@ VecN n = One / pure n
ListN : Normal
ListN = Nat / id

-- These exercises don't appear anywhere, but we did cover them during
-- the lecture. I added a placemarker in the notes for this.

K : Set -> Normal
K A = {!!}
Expand Down
5 changes: 4 additions & 1 deletion Vec.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -684,6 +684,9 @@ Note that |<?>| has been defined to work at all levels of the predicative
hierarchy, so that we can use it to choose between |Set|s, as well as between
ordinary values. |Sg| thus models both choice and pairing in data structures.

TODO: Insert exercise/comment regarding constant functors and the
identity being normal.

I don't know about you, but I find I do a lot more arithmetic with types than I
do with numbers, which is why I have used |*| and |+| for |Set|s. Developing a
library of normal functors will, however, necessitate arithmetic on sizes as
Expand Down Expand Up @@ -767,7 +770,7 @@ nOut : forall {X}(F G : Normal) -> <! F +N G !>N X -> <! F !>N X + <! G !>N X
nOut F G xs' with nCase F G xs'
nOut F G .(nInj F G xs) | from xs = xs
\end{code}
The |with| notation allows us to compute smoe useful information and add
The |with| notation allows us to compute some useful information and add
it to the collection of things available for inspection in pattern matching.
By matching the result of |nCase F G xs'| as |from xs|, we discover that
\emph{ipso facto}, |xs'| is |nInj xs|. It is in the nature of dependent
Expand Down