diff --git a/Agda.css b/Agda.css new file mode 100644 index 0000000..dee5578 --- /dev/null +++ b/Agda.css @@ -0,0 +1,467 @@ +/*! normalize.css v2.1.3 | MIT License | git.io/normalize */ + +/* ========================================================================== + HTML5 display definitions + ========================================================================== */ + +/** + * Correct `block` display not defined in IE 8/9. + */ + + article, + aside, + details, + figcaption, + figure, + footer, + header, + hgroup, + main, + nav, + section, + summary { + display: block; + } + + /** + * Correct `inline-block` display not defined in IE 8/9. + */ + + audio, + canvas, + video { + display: inline-block; + } + + /** + * Prevent modern browsers from displaying `audio` without controls. + * Remove excess height in iOS 5 devices. + */ + + audio:not([controls]) { + display: none; + height: 0; + } + + /** + * Address `[hidden]` styling not present in IE 8/9. + * Hide the `template` element in IE, Safari, and Firefox < 22. + */ + + [hidden], + template { + display: none; + } + + /* ========================================================================== + Base + ========================================================================== */ + + /** + * 1. Set default font family to sans-serif. + * 2. Prevent iOS text size adjust after orientation change, without disabling + * user zoom. + */ + + html { + font-family: sans-serif; /* 1 */ + -ms-text-size-adjust: 100%; /* 2 */ + -webkit-text-size-adjust: 100%; /* 2 */ + } + + /** + * Remove default margin. + */ + + body { + margin: 0; + } + + /* ========================================================================== + Links + ========================================================================== */ + + /** + * Remove the gray background color from active links in IE 10. + */ + + a { + background: transparent; + } + + /** + * Address `outline` inconsistency between Chrome and other browsers. + */ + + a:focus { + outline: thin dotted; + } + + /** + * Improve readability when focused and also mouse hovered in all browsers. + */ + + a:active, + a:hover { + outline: 0; + } + + /* ========================================================================== + Typography + ========================================================================== */ + + /** + * Address variable `h1` font-size and margin within `section` and `article` + * contexts in Firefox 4+, Safari 5, and Chrome. + */ + + h1 { + font-size: 2em; + margin: 0.67em 0; + } + + /** + * Address styling not present in IE 8/9, Safari 5, and Chrome. + */ + + abbr[title] { + border-bottom: 1px dotted; + } + + /** + * Address style set to `bolder` in Firefox 4+, Safari 5, and Chrome. + */ + + b, + strong { + font-weight: bold; + } + + /** + * Address styling not present in Safari 5 and Chrome. + */ + + dfn { + font-style: italic; + } + + /** + * Address differences between Firefox and other browsers. + */ + + hr { + -moz-box-sizing: content-box; + box-sizing: content-box; + height: 0; + } + + /** + * Address styling not present in IE 8/9. + */ + + mark { + background: #ff0; + color: #000; + } + + /** + * Correct font family set oddly in Safari 5 and Chrome. + */ + + code, + kbd, + pre, + samp { + font-family: monospace, serif; + font-size: 1em; + } + + /** + * Improve readability of pre-formatted text in all browsers. + */ + + pre { + white-space: pre; + overflow-x: scroll; + } + + /** + * Set consistent quote types. + */ + + q { + quotes: "\201C" "\201D" "\2018" "\2019"; + } + + /** + * Address inconsistent and variable font size in all browsers. + */ + + small { + font-size: 80%; + } + + /** + * Prevent `sub` and `sup` affecting `line-height` in all browsers. + */ + + sub, + sup { + font-size: 75%; + line-height: 0; + position: relative; + vertical-align: baseline; + } + + sup { + top: -0.5em; + } + + sub { + bottom: -0.25em; + } + + /* ========================================================================== + Embedded content + ========================================================================== */ + + /** + * Remove border when inside `a` element in IE 8/9. + */ + + img { + border: 0; + } + + /** + * Correct overflow displayed oddly in IE 9. + */ + + svg:not(:root) { + overflow: hidden; + } + + /* ========================================================================== + Figures + ========================================================================== */ + + /** + * Address margin not present in IE 8/9 and Safari 5. + */ + + figure { + margin: 0; + } + + /* ========================================================================== + Forms + ========================================================================== */ + + /** + * Define consistent border, margin, and padding. + */ + + fieldset { + border: 1px solid #c0c0c0; + margin: 0 2px; + padding: 0.35em 0.625em 0.75em; + } + + /** + * 1. Correct `color` not being inherited in IE 8/9. + * 2. Remove padding so people aren't caught out if they zero out fieldsets. + */ + + legend { + border: 0; /* 1 */ + padding: 0; /* 2 */ + } + + /** + * 1. Correct font family not being inherited in all browsers. + * 2. Correct font size not being inherited in all browsers. + * 3. Address margins set differently in Firefox 4+, Safari 5, and Chrome. + */ + + button, + input, + select, + textarea { + font-family: inherit; /* 1 */ + font-size: 100%; /* 2 */ + margin: 0; /* 3 */ + } + + /** + * Address Firefox 4+ setting `line-height` on `input` using `!important` in + * the UA stylesheet. + */ + + button, + input { + line-height: normal; + } + + /** + * Address inconsistent `text-transform` inheritance for `button` and `select`. + * All other form control elements do not inherit `text-transform` values. + * Correct `button` style inheritance in Chrome, Safari 5+, and IE 8+. + * Correct `select` style inheritance in Firefox 4+ and Opera. + */ + + button, + select { + text-transform: none; + } + + /** + * 1. Avoid the WebKit bug in Android 4.0.* where (2) destroys native `audio` + * and `video` controls. + * 2. Correct inability to style clickable `input` types in iOS. + * 3. Improve usability and consistency of cursor style between image-type + * `input` and others. + */ + + button, + html input[type="button"], /* 1 */ + input[type="reset"], + input[type="submit"] { + -webkit-appearance: button; /* 2 */ + cursor: pointer; /* 3 */ + } + + /** + * Re-set default cursor for disabled elements. + */ + + button[disabled], + html input[disabled] { + cursor: default; + } + + /** + * 1. Address box sizing set to `content-box` in IE 8/9/10. + * 2. Remove excess padding in IE 8/9/10. + */ + + input[type="checkbox"], + input[type="radio"] { + box-sizing: border-box; /* 1 */ + padding: 0; /* 2 */ + } + + /** + * 1. Address `appearance` set to `searchfield` in Safari 5 and Chrome. + * 2. Address `box-sizing` set to `border-box` in Safari 5 and Chrome + * (include `-moz` to future-proof). + */ + + input[type="search"] { + -webkit-appearance: textfield; /* 1 */ + -moz-box-sizing: content-box; + -webkit-box-sizing: content-box; /* 2 */ + box-sizing: content-box; + } + + /** + * Remove inner padding and search cancel button in Safari 5 and Chrome + * on OS X. + */ + + input[type="search"]::-webkit-search-cancel-button, + input[type="search"]::-webkit-search-decoration { + -webkit-appearance: none; + } + + /** + * Remove inner padding and border in Firefox 4+. + */ + + button::-moz-focus-inner, + input::-moz-focus-inner { + border: 0; + padding: 0; + } + + /** + * 1. Remove default vertical scrollbar in IE 8/9. + * 2. Improve readability and alignment in all browsers. + */ + + textarea { + overflow: auto; /* 1 */ + vertical-align: top; /* 2 */ + } + + /* ========================================================================== + Tables + ========================================================================== */ + + /** + * Remove most spacing between table cells. + */ + + table { + border-collapse: collapse; + border-spacing: 0; + } + + .go-top { + position: fixed; + bottom: 2em; + right: 2em; + text-decoration: none; + background-color: #E0E0E0; + font-size: 12px; + padding: 1em; + display: inline; + } + + /* Github css */ + + html,body{ margin: auto; + padding-right: 1em; + padding-left: 1em; + color:black;}*:not('#mkdbuttons'){margin:0;padding:0}body{font:13.34px helvetica,arial,freesans,clean,sans-serif;-webkit-font-smoothing:subpixel-antialiased;line-height:1.4;padding:3px;background:#fff;border-radius:3px;-moz-border-radius:3px;-webkit-border-radius:3px}p{margin:1em 0}a{color:#4183c4;text-decoration:none}body{background-color:#fff;padding:30px;margin:15px;font-size:14px;line-height:1.6}body>*:first-child{margin-top:0!important}body>*:last-child{margin-bottom:0!important}@media screen{body{box-shadow:0 0 0 1px #cacaca,0 0 0 4px #eee}}h1,h2,h3,h4,h5,h6{margin:20px 0 10px;padding:0;font-weight:bold;-webkit-font-smoothing:subpixel-antialiased;cursor:text}h1{font-size:28px;color:#000}h2{font-size:24px;border-bottom:1px solid #ccc;color:#000}h3{font-size:18px;color:#333}h4{font-size:16px;color:#333}h5{font-size:14px;color:#333}h6{color:#777;font-size:14px}p,blockquote,table,pre{margin:15px 0}ul{padding-left:30px}ol{padding-left:30px}ol li ul:first-of-type{margin-top:0}hr{background:transparent url(data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAYAAAAECAYAAACtBE5DAAAAGXRFWHRTb2Z0d2FyZQBBZG9iZSBJbWFnZVJlYWR5ccllPAAAAyJpVFh0WE1MOmNvbS5hZG9iZS54bXAAAAAAADw/eHBhY2tldCBiZWdpbj0i77u/IiBpZD0iVzVNME1wQ2VoaUh6cmVTek5UY3prYzlkIj8+IDx4OnhtcG1ldGEgeG1sbnM6eD0iYWRvYmU6bnM6bWV0YS8iIHg6eG1wdGs9IkFkb2JlIFhNUCBDb3JlIDUuMC1jMDYwIDYxLjEzNDc3NywgMjAxMC8wMi8xMi0xNzozMjowMCAgICAgICAgIj4gPHJkZjpSREYgeG1sbnM6cmRmPSJodHRwOi8vd3d3LnczLm9yZy8xOTk5LzAyLzIyLXJkZi1zeW50YXgtbnMjIj4gPHJkZjpEZXNjcmlwdGlvbiByZGY6YWJvdXQ9IiIgeG1sbnM6eG1wPSJodHRwOi8vbnMuYWRvYmUuY29tL3hhcC8xLjAvIiB4bWxuczp4bXBNTT0iaHR0cDovL25zLmFkb2JlLmNvbS94YXAvMS4wL21tLyIgeG1sbnM6c3RSZWY9Imh0dHA6Ly9ucy5hZG9iZS5jb20veGFwLzEuMC9zVHlwZS9SZXNvdXJjZVJlZiMiIHhtcDpDcmVhdG9yVG9vbD0iQWRvYmUgUGhvdG9zaG9wIENTNSBNYWNpbnRvc2giIHhtcE1NOkluc3RhbmNlSUQ9InhtcC5paWQ6OENDRjNBN0E2NTZBMTFFMEI3QjRBODM4NzJDMjlGNDgiIHhtcE1NOkRvY3VtZW50SUQ9InhtcC5kaWQ6OENDRjNBN0I2NTZBMTFFMEI3QjRBODM4NzJDMjlGNDgiPiA8eG1wTU06RGVyaXZlZEZyb20gc3RSZWY6aW5zdGFuY2VJRD0ieG1wLmlpZDo4Q0NGM0E3ODY1NkExMUUwQjdCNEE4Mzg3MkMyOUY0OCIgc3RSZWY6ZG9jdW1lbnRJRD0ieG1wLmRpZDo4Q0NGM0E3OTY1NkExMUUwQjdCNEE4Mzg3MkMyOUY0OCIvPiA8L3JkZjpEZXNjcmlwdGlvbj4gPC9yZGY6UkRGPiA8L3g6eG1wbWV0YT4gPD94cGFja2V0IGVuZD0iciI/PqqezsUAAAAfSURBVHjaYmRABcYwBiM2QSA4y4hNEKYDQxAEAAIMAHNGAzhkPOlYAAAAAElFTkSuQmCC) repeat-x 0 0;border:0 none;color:#ccc;height:4px;padding:0}body>h2:first-child{margin-top:0;padding-top:0}body>h1:first-child{margin-top:0;padding-top:0}body>h1:first-child+h2{margin-top:0;padding-top:0}body>h3:first-child,body>h4:first-child,body>h5:first-child,body>h6:first-child{margin-top:0;padding-top:0}a:first-child h1,a:first-child h2,a:first-child h3,a:first-child h4,a:first-child h5,a:first-child h6{margin-top:0;padding-top:0}h1+p,h2+p,h3+p,h4+p,h5+p,h6+p,ul li>:first-child,ol li>:first-child{margin-top:0}dl{padding:0}dl dt{font-size:14px;font-weight:bold;font-style:italic;padding:0;margin:15px 0 5px}dl dt:first-child{padding:0}dl dt>:first-child{margin-top:0}dl dt>:last-child{margin-bottom:0}dl dd{margin:0 0 15px;padding:0 15px}dl dd>:first-child{margin-top:0}dl dd>:last-child{margin-bottom:0}blockquote{border-left:4px solid #DDD;padding:0 15px;color:#777}blockquote>:first-child{margin-top:0}blockquote>:last-child{margin-bottom:0}table{border-collapse:collapse;border-spacing:0;font-size:100%;font:inherit}table th{font-weight:bold;border:1px solid #ccc;padding:6px 13px}table td{border:1px solid #ccc;padding:6px 13px}table tr{border-top:1px solid #ccc;background-color:#fff}table tr:nth-child(2n){background-color:#f8f8f8}img{max-width:100%}code,tt{margin:0 2px;padding:0 5px;white-space:nowrap;border:1px solid #eaeaea;background-color:#f8f8f8;border-radius:3px;font-family:Consolas,'Liberation Mono',Courier,monospace;font-size:12px;color:#333}pre>code{margin:0;padding:0;white-space:pre;border:0;background:transparent}.highlight pre{background-color:#f8f8f8;border:1px solid #ccc;font-size:13px;line-height:19px;overflow:auto;padding:6px 10px;border-radius:3px}pre{background-color:#f8f8f8;border:1px solid #ccc;font-size:13px;line-height:19px;overflow:auto;padding:6px 10px;border-radius:3px}pre code,pre tt{background-color:transparent;border:0}.poetry pre{font-family:Georgia,Garamond,serif!important;font-style:italic;font-size:110%!important;line-height:1.6em;display:block;margin-left:1em}.poetry pre code{font-family:Georgia,Garamond,serif!important;word-break:break-all;word-break:break-word;-webkit-hyphens:auto;-moz-hyphens:auto;hyphens:auto;white-space:pre-wrap}sup,sub,a.footnote{font-size:1.4ex;height:0;line-height:1;vertical-align:super;position:relative}sub{vertical-align:sub;top:-1px}@media print{body{background:#fff}img,pre,blockquote,table,figure{page-break-inside:avoid}body{background:#fff;border:0}code{background-color:#fff;color:#333!important;padding:0 .2em;border:1px solid #dedede}pre{background:#fff}pre code{background-color:white!important;overflow:visible}}@media screen{body.inverted{color:#eee!important;border-color:#555;box-shadow:none}.inverted body,.inverted hr .inverted p,.inverted td,.inverted li,.inverted h1,.inverted h2,.inverted h3,.inverted h4,.inverted h5,.inverted h6,.inverted th,.inverted .math,.inverted caption,.inverted dd,.inverted dt,.inverted blockquote{color:#eee!important;border-color:#555;box-shadow:none}.inverted td,.inverted th{background:#333}.inverted h2{border-color:#555}.inverted hr{border-color:#777;border-width:1px!important}::selection{background:rgba(157,193,200,0.5)}h1::selection{background-color:rgba(45,156,208,0.3)}h2::selection{background-color:rgba(90,182,224,0.3)}h3::selection,h4::selection,h5::selection,h6::selection,li::selection,ol::selection{background-color:rgba(133,201,232,0.3)}code::selection{background-color:rgba(0,0,0,0.7);color:#eee}code span::selection{background-color:rgba(0,0,0,0.7)!important;color:#eee!important}a::selection{background-color:rgba(255,230,102,0.2)}.inverted a::selection{background-color:rgba(255,230,102,0.6)}td::selection,th::selection,caption::selection{background-color:rgba(180,237,95,0.5)}.inverted{background:#0b2531;background:#252a2a}.inverted body{background:#252a2a}.inverted a{color:#acd1d5}}.highlight .c{color:#998;font-style:italic}.highlight .err{color:#a61717;background-color:#e3d2d2}.highlight .k,.highlight .o{font-weight:bold}.highlight .cm{color:#998;font-style:italic}.highlight .cp{color:#999;font-weight:bold}.highlight .c1{color:#998;font-style:italic}.highlight .cs{color:#999;font-weight:bold;font-style:italic}.highlight .gd{color:#000;background-color:#fdd}.highlight .gd .x{color:#000;background-color:#faa}.highlight .ge{font-style:italic}.highlight .gr{color:#a00}.highlight .gh{color:#999}.highlight .gi{color:#000;background-color:#dfd}.highlight .gi .x{color:#000;background-color:#afa}.highlight .go{color:#888}.highlight .gp{color:#555}.highlight .gs{font-weight:bold}.highlight .gu{color:#800080;font-weight:bold}.highlight .gt{color:#a00}.highlight .kc,.highlight .kd,.highlight .kn,.highlight .kp,.highlight .kr{font-weight:bold}.highlight .kt{color:#458;font-weight:bold}.highlight .m{color:#099}.highlight .s{color:#d14}.highlight .na{color:#008080}.highlight .nb{color:#0086b3}.highlight .nc{color:#458;font-weight:bold}.highlight .no{color:#008080}.highlight .ni{color:#800080}.highlight .ne,.highlight .nf{color:#900;font-weight:bold}.highlight .nn{color:#555}.highlight .nt{color:#000080}.highlight .nv{color:#008080}.highlight .ow{font-weight:bold}.highlight .w{color:#bbb}.highlight .mf,.highlight .mh,.highlight .mi,.highlight .mo{color:#099}.highlight .sb,.highlight .sc,.highlight .sd,.highlight .s2,.highlight .se,.highlight .sh,.highlight .si,.highlight .sx{color:#d14}.highlight .sr{color:#009926}.highlight .s1{color:#d14}.highlight .ss{color:#990073}.highlight .bp{color:#999}.highlight .vc,.highlight .vg,.highlight .vi{color:#008080}.highlight .il{color:#099}.highlight .gc{color:#999;background-color:#eaf2f5}.type-csharp .highlight .k,.type-csharp .highlight .kt{color:#00F}.type-csharp .highlight .nf{color:#000;font-weight:normal}.type-csharp .highlight .nc{color:#2b91af}.type-csharp .highlight .nn{color:#000}.type-csharp .highlight .s,.type-csharp .highlight .sc{color:#a31515} + +/* Aspects. */ +.Agda .Comment { color: #B22222 } +.Agda .Background { color: #000000 } +.Agda .Markup { color: #000000 } +.Agda .Keyword { color: #CD6600 } +.Agda .String { color: #B22222 } +.Agda .Number { color: #A020F0 } +.Agda .Symbol { color: #404040 } +.Agda .PrimitiveType { color: #0000CD } +.Agda .Pragma { color: black } +.Agda .Operator {} +.Agda .Hole { background: #B4EEB4 } + +/* NameKinds. */ +.Agda .Bound { color: black } +.Agda .Generalizable { color: black } +.Agda .InductiveConstructor { color: #008B00 } +.Agda .CoinductiveConstructor { color: #8B7500 } +.Agda .Datatype { color: #0000CD } +.Agda .Field { color: #EE1289 } +.Agda .Function { color: #0000CD } +.Agda .Module { color: #A020F0 } +.Agda .Postulate { color: #0000CD } +.Agda .Primitive { color: #0000CD } +.Agda .Record { color: #0000CD } + +/* OtherAspects. */ +.Agda .DottedPattern {} +.Agda .UnsolvedMeta { color: black; background: yellow } +.Agda .UnsolvedConstraint { color: black; background: yellow } +.Agda .TerminationProblem { color: black; background: #FFA07A } +.Agda .IncompletePattern { color: black; background: #F5DEB3 } +.Agda .Error { color: red; text-decoration: underline } +.Agda .TypeChecks { color: black; background: #ADD8E6 } +.Agda .Deadcode { color: black; background: #808080 } +.Agda .ShadowingInTelescope { color: black; background: #808080 } + +/* Standard attributes. */ +.Agda a { text-decoration: none } +.Agda a[href]:hover { background-color: #B4EEB4 } +.Agda [href].hover-highlight { background-color: #B4EEB4; } diff --git a/Literature.md b/Literature.md new file mode 100644 index 0000000..e42eba8 --- /dev/null +++ b/Literature.md @@ -0,0 +1,5 @@ +# Literature +1. *The* paper https://arxiv.org/pdf/2102.11828.pdf +2. Delay Monad by Capretta https://arxiv.org/pdf/cs/0505037.pdf +3. Altenkirch et al. show problems of the delay monad https://arxiv.org/pdf/1610.09254.pdf +4. Chapman et al. agda formalization of the delay monad https://niccoloveltri.github.io/mscs_final.pdf \ No newline at end of file diff --git a/Makefile b/Makefile index f2a2a0f..355ac99 100644 --- a/Makefile +++ b/Makefile @@ -5,11 +5,13 @@ all: agda pandoc: public/*.md @$(foreach file,$^, \ - pandoc $(file) -s -c Agda.css -o $(file:.md=.html) ; \ + pandoc $(file) -s --to=html+TEX_MATH_DOLLARS --mathjax -c Agda.css -o $(file:.md=.html) ; \ ) agda: Everything.agda agda --html --html-dir=public Everything.agda --html-highlight=auto -i. + rm -f public/Agda.css + cp Agda.css public/Agda.css mv public/Everything.html public/index.html clean: @@ -17,9 +19,6 @@ clean: rm -rf public/* find . -name '*.agdai' -exec rm \{\} \; -open: - firefox public/Everything.html - # push compiled html to my cip directory push: all push' diff --git a/src/Algebra/Elgot/Properties.lagda.md b/src/Algebra/Elgot/Properties.lagda.md index 85979f8..4ef47b4 100644 --- a/src/Algebra/Elgot/Properties.lagda.md +++ b/src/Algebra/Elgot/Properties.lagda.md @@ -1,5 +1,6 @@ ## Summary -A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satiesfies +A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satisfies - α now ≈ id - α ▷ ≈ α diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index f4ef477..fd2d782 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -20,6 +20,7 @@ import Categories.Morphism.Reasoning as MR' ## Summary We work in an ambient category that + - is extensive (has finite coproducts and pullbacks along injections) - is cartesian (has finite products, extensive + cartesian also gives a distributivity isomorphism) - has a parametrized NNO ℕ diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index c022274..4599027 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/src/Monad/Instance/Delay.lagda.md @@ -14,16 +14,21 @@ open import Categories.Category.Construction.F-Coalgebras open import Category.Instance.AmbientCategory using (Ambient) ``` --> - -## Summary -This file introduces the delay monad ***D*** - -## Code - ```agda module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where open Ambient ambient ``` + +## Definition + +The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523) + +We will now define it categorically by existence of final coalgebras for the functor `(X + -)` where `X` is some object. +This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`. + +In this definition `D X` is the underlying object of the final coalgebra given by `X`. +We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inverse can be factored into the constructors `now` and `later`. + -The Delay monad is usually described by existence of final coalgebras for the functor `(X + -)` where `X` is some arbitrary object. -This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`. - ```agda record DelayM : Set (o ⊔ ℓ ⊔ e) where field coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-)) -``` - -These are all the fields this record needs! -Of course this doesn't tell us very much, so our goal will be to extract a monad from this definition. - -Conventionally the delay monad is described via functions `now` and `later` where the former lifts a value into a computation and the latter postpones a computation by one time unit. -We can now define these functions by bisecting the isomorphism `out : DX ≅ X + DX` which we get by Lambek's lemma. (Here `DX` is the element of the final coalgebra for `X`) - -```agda module _ {X : Obj} where open Terminal (coalgebras X) using (⊤; !; !-unique) @@ -79,9 +72,10 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X + ``` -Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`: +Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`: -TODO add diagram + + ```agda module _ {Y : Obj} where @@ -92,31 +86,41 @@ TODO add diagram coit-commutes f = commutes (! {A = record { A = Y ; α = f }}) ``` -If we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`. +Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`. At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras. -TODO add diagram + + ```agda - iso : X × N ≅ X + X × N - iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X }) + nno-iso : X × N ≅ X + X × N + nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X }) ι : X × N ⇒ DX - ι = u (! {A = record { A = X × N ; α = _≅_.from iso }}) + ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }}) ``` -Make `DX` conveniently accessible + +## Delay is a monad + +The next step is showing that this actually yields a monad. Some parts for this are already given, we can construct `D X` from `X` and `now : D X ⇒ D X` is the monad unit. +What's missing is Kleisli-lifting, given a morphism `f : X ⇒ D Y` we need to construct a morphism `extend f : D X ⇒ D Y`. +To do so we go from `D X` to `D X + D Y` via injection and then construct a coalgebra `D X + D Y ⇒ Y + (D X + D Y)`, the final coalgebra `D Y ⇒ Y + D Y` then yields a coalgebra-morphism from `D X + D Y` to `D Y`, see the following diagram: + + + + +Proving the monad laws then requires two key lemmas, first of all that the following diagram commutes for any `f` (this is `extendlaw`) + + + + +and second that `extend f` is the unique morphism satisfying the commutative diagram i.e. any other morphism for which the diagram commutes must be equivalent to `extend f` (this is `extend-unique`). + ```agda + -- Make DX more accessible outside D₀ : Obj → Obj D₀ X = DX {X} -``` -With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`. -`F₀` corresponds to `D₀` of course and `unit` is `now`, the tricky part is kleisli lifting aka. `extend`. - -TODO - - -```agda kleisli : KleisliTriple C kleisli = record { F₀ = D₀ @@ -277,11 +281,3 @@ TODO functor : Endofunctor C functor = Monad.F monad ``` - -### Definition 30: Search-Algebras - -TODO - -### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras - -TODO