body,html{font-family:'Open Sans',sans-serif;font-display:swap;font-variant-ligatures:common-ligatures discretionary-ligatures contextual;text-rendering:optimizeLegibility;font-size:18px}body{width:100%;color:#b0b0b0;background-color:#2b2b2b;overflow-x:hidden;margin:0}it{font-style:italic}b{font-style:bold}#wrapper{padding-top:20px;margin-left:auto;margin-right:auto;transition:opacity .5s linear;opacity:1}#wrapper.updating{opacity:0}.info-hdr{position:relative;min-width:450;padding-left:10px;padding-right:10px;box-sizing:border-box}main{padding-left:10px;padding-right:10px;box-sizing:border-box;min-height:100vh}main>header .section_h{width:100%}.license{font-variant:small-caps}.post main{padding-bottom:60px;padding-top:0}.small *{font-size:.6em;line-height:12pt}ul{list-style:circle}ul.blog-posts{list-style:none}ul.blog-posts>li{padding-top:5px;padding-bottom:5px}.blog-posts h1{display:inline;font-size:1.1em;margin-bottom:5px;color:#41a294}.blog-posts p{margin-top:5px;margin-bottom:5px;padding-left:30px}.blog-posts .date{font-size:.8em;margin-left:30px}.blog-posts .links{list-style:none;font-size:small}.langs{margin-top:10px}.clearfix{clear:both}img{border:0}.info-hdr img.me{display:block;width:250px;-webkit-border-radius:50%;-moz-border-radius:50%;-ms-border-radius:50%;-o-border-radius:50%;border-radius:50%;margin:10px auto 20px;-webkit-box-shadow:0 0 10px #444;-moz-box-shadow:0 0 10px #444;-ms-box-shadow:0 0 10px #444;-o-box-shadow:0 0 10px #444;box-shadow:0 0 10px #444}.info-hdr p{margin-top:.5em;margin-bottom:.5em}.info-hdr .links{list-style:none;margin:0;padding-left:0;padding-inline-start:0}.info-hdr .links li.rss{margin-left:15px}.info-hdr .links li{margin-left:5px;display:inline-block}.info-hdr .links li.right{float:right}.post .info-hdr{min-width:200px}.post .info-hdr .links .about{display:none}pre{padding:10px;border-radius:1px}code,pre{font-family:"Roboto Mono Light","Cutive Mono",monospace;color:#a0a0a0}pre.sourceCode{overflow:visible}pre.haskell{border-radius:1px;white-space:pre}pre.Agda a,pre.haskell a{color:inherit}.Agda .Datatype,.Agda .InductiveConstructor,.Agda .PrimitiveType,.haskell .dt,.haskell .kw{font-weight:700}.Agda .Keyword{color:#536cff}.Agda .Symbol,.haskell .op{color:#536dff}.Agda .Comment,.haskell .co{color:#989898}.mjx-chtml.MathJax_CHTML{font-size:1.1em!important}.mjx-chtml.MJXc-display{display:block;font-size:.9em;padding:10px 20px;color:#a0a0a0}.diagram,.post figure{margin:0;max-width:600px;display:block;padding:10px 20px;color:#505050}.diagram img,.post figure img{max-width:100%;display:block;margin:0 auto}.post figure{padding-left:0;padding-right:0;margin:0 auto;min-width:100%}.post figure.small img{max-width:350px}.post figure.large img{width:100%}.post .video iframe{display:block;margin-left:auto;margin-right:auto}.post figure figcaption{text-align:center}.post figure figcaption.left{text-align:left}.post figure img[src="/images/one-object-cat.svg"]{max-height:150px}.post figure img[src="/images/tr-graph.svg"]{max-height:300px}@-webkit-keyframes rotate{from{-webkit-transform:rotateZ(0);-moz-transform:rotateZ(0);-ms-transform:rotateZ(0);-o-transform:rotateZ(0);transform:rotateZ(0)}to{-webkit-transform:rotateZ(360deg);-moz-transform:rotateZ(360deg);-ms-transform:rotateZ(360deg);-o-transform:rotateZ(360deg);transform:rotateZ(360deg)}}@-moz-keyframes rotate{from{-webkit-transform:rotateZ(0);-moz-transform:rotateZ(0);-ms-transform:rotateZ(0);-o-transform:rotateZ(0);transform:rotateZ(0)}to{-webkit-transform:rotateZ(360deg);-moz-transform:rotateZ(360deg);-ms-transform:rotateZ(360deg);-o-transform:rotateZ(360deg);transform:rotateZ(360deg)}}@-o-keyframes rotate{from{-webkit-transform:rotateZ(0);-moz-transform:rotateZ(0);-ms-transform:rotateZ(0);-o-transform:rotateZ(0);transform:rotateZ(0)}to{-webkit-transform:rotateZ(360deg);-moz-transform:rotateZ(360deg);-ms-transform:rotateZ(360deg);-o-transform:rotateZ(360deg);transform:rotateZ(360deg)}}@keyframes rotate{from{-webkit-transform:rotateZ(0);-moz-transform:rotateZ(0);-ms-transform:rotateZ(0);-o-transform:rotateZ(0);transform:rotateZ(0)}to{-webkit-transform:rotateZ(360deg);-moz-transform:rotateZ(360deg);-ms-transform:rotateZ(360deg);-o-transform:rotateZ(360deg);transform:rotateZ(360deg)}}.info-hdr #name{color:#e0e0e0;font-weight:300;font-size:1.6em;text-align:center}.info-hdr #name .subtitle{font-size:.9em;width:100%;margin:0 auto}.info-hdr p{font-weight:300;font-size:1.2em}section{margin-bottom:40px}ul>li section{margin-top:5px;margin-bottom:15px}article{margin-bottom:40px}@media screen and (min-width:921px) and (min-height:500px){#wrapper{width:920px}.info-hdr{float:left;width:380px;position:fixed}.info-hdr #name{text-align:left}.post .info-hdr{float:none;width:740px;position:static;margin-left:auto;margin-right:auto;height:auto}main{float:right;width:540px}.post main{width:740px;float:none;margin-left:auto;margin-right:auto}@supports (display:flex){.info-hdr{display:flex;flex-direction:column;justify-content:center}}}@media screen and (max-width:920px),screen and (max-height:500px){#wrapper{width:100%;min-width:300px}.info-hdr{max-width:450px;margin-left:auto;margin-right:auto;padding:10px}.info-hdr #name{text-align:left}.post .info-hdr{max-width:740px}main{max-width:540px;margin-left:auto;margin-right:auto;padding:10px}.post main{max-width:740px}}@media screen and (max-width:600px){.mjx-chtml.MJXc-display,pre.haskell code{font-size:.8em}.diagram img{max-width:70vw}}@media screen and (max-width:400px){.mjx-chtml.MJXc-display,pre.haskell code{font-size:.7em}}footer{margin-top:20px;margin-bottom:20px;margin-left:auto;margin-right:auto;font-size:.8rem;text-align:center}.post_footer{display:flex;margin-top:40px}.post_footer .home{flex:1 0 10%;text-align:left}.post_footer .comment{flex:1 0 30%;text-align:left}.post_footer .twitter{flex:1 0 40%;font-style:italic;text-align:right}.post_footer .rss{flex:1 0 10%;font-style:italic;text-align:right}.btn{display:inline-block;padding:6px 12px;color:#333;border:1px solid #ccc;border-radius:5px;text-decoration:none;text-align:center;user-select:none;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;-o-user-select:none;user-select:none}.btn:visited{color:inherit;border:0}a{color:#536cff;text-decoration:none}address{margin-top:10px;font-size:.85em}address .social{margin-top:10px}.social a{display:inline-block}a .icon{width:18px;vertical-align:middle}@-webkit-keyframes fly{0%{top:0;left:0;opacity:1}50%{top:-10px;left:15px;opacity:.6}80%{top:-20px;left:40px;opacity:0}81%{top:0;left:0;opacity:0}100%{top:0;left:0;opacity:1}}@-moz-keyframes fly{0%{top:0;left:0;opacity:1}50%{top:-10px;left:15px;opacity:.6}80%{top:-20px;left:40px;opacity:0}81%{top:0;left:0;opacity:0}100%{top:0;left:0;opacity:1}}@-o-keyframes fly{0%{top:0;left:0;opacity:1}50%{top:-10px;left:15px;opacity:.6}80%{top:-20px;left:40px;opacity:0}81%{top:0;left:0;opacity:0}100%{top:0;left:0;opacity:1}}@keyframes fly{0%{top:0;left:0;opacity:1}50%{top:-10px;left:15px;opacity:.6}80%{top:-20px;left:40px;opacity:0}81%{top:0;left:0;opacity:0}100%{top:0;left:0;opacity:1}}.social>a{position:relative;padding-left:5px;padding-right:5px}.social>a #rss_i,.social>a #twitter_i{top:4px}.contents h3{margin-bottom:5px}.contents ol{margin-top:5px;padding-left:15px}#twitter i.fa.animate{-webkit-animation:fly 1s ease 0s 1;-moz-animation:fly 1s ease 0s 1;-ms-animation:fly 1s ease 0s 1;-o-animation:fly 1s ease 0s 1;animation:fly 1s ease 0s 1}.badge{display:inline-block;padding:3px 6px 5px 6px;margin:4px 2px;border-radius:2px;color:#222;background-color:#e6e6e6;-webkit-box-shadow:1px 1px 3px #f0f0f0;-moz-box-shadow:1px 1px 3px #f0f0f0;-ms-box-shadow:1px 1px 3px #f0f0f0;box-shadow:1px 1px 3px #f0f0f0;font-variant:all-small-caps;font-size:.9em;line-height:1em;font-weight:300}.badge{color:#222;background-color:#e6e6e6;font-weight:600;-webkit-box-shadow:1px 1px 3px #f0f0f0;-moz-box-shadow:1px 1px 3px #f0f0f0;-ms-box-shadow:1px 1px 3px #f0f0f0;box-shadow:1px 1px 3px #f0f0f0}.cv,.hidden{display:none}.about .cv{visibility:hidden}.badge.cv{margin-top:10px;width:100px;text-align:center;cursor:pointer;font-weight:300}.cv:hover{box-shadow:1px 1px 1px #aaa}section{padding-right:10px}.print_only{display:none}.section_h{font-weight:300}.post h1{width:100%;border-bottom:1px solid #e0e0e0;font-weight:300;color:#e0e0e0}.post h2{font-weight:300;color:#e0e0e0}.post h3{font-weight:300;color:#e0e0e0}.post h4{font-weight:200;color:#e0e0e0}.post #img_container{display:none}.post header address{display:none}.bio h4{font-weight:300;font-variant-caps:all-small-caps;margin-top:8px;margin-bottom:5px}.portfolio h3{font-weight:300;margin-bottom:.2em}.portfolio h3 .title:before{font-weight:300;margin-right:2px;content:"•••"}.portfolio h3 a{color:inherit}.portfolio h3 a i.fa{color:#888}.portfolio h3 a:visited i.fa{color:#ccc}.papers ul{list-style:none;-webkit-padding-start:0;padding-inline-start:0}.papers>ul>li:not(:first-child){margin-top:10px}.journal{font-variant:small-caps;text-transform:uppercase}.journal span{font-variant-caps:all-small-caps;text-transform:none}.authors{list-style:none;-webkit-padding-start:0;padding-inline-start:0}.authors>li{display:inline-block;margin-right:2px;font-style:italic}.authors li:not(:last-child):after{content:","}.definition,.proof,.proposition{margin-top:10px;margin-bottom:10px;padding-left:1em}.definition h6,.proposition h6{display:inline-block;margin:0;margin-bottom:3px;font-size:1em;font-weight:500}.proposition h6{display:block}.definition h6 span:first-child,.proof h6,.proposition h6 span:first-child{font-size:large;font-weight:300;margin-bottom:3px;margin-right:5px}.ups{display:block;max-width:500px;font-size:2em;font-weight:lighter;margin:100px auto 100px;text-align:center;color:#434343}.ups:active,.ups:focus,.ups:visited{color:#434343}.ups img{display:block;margin:100px auto 20px;width:100%;max-width:200px}.qed{display:block;position:relative;top:-10px;text-transform:lowercase;font-variant:small-caps;font-weight:700}.lemma{padding-left:20px}blockquote{background-color:#4b4b4b;padding:5px 40px;margin:10px 10px}blockquote ul{padding-left:0;padding-right:0}