html{font-size:110%;font-family:sans-serif;background-color:#fcfcfc}body{margin:2em auto;padding:0px 1em;max-width:800px;line-height:1.4;color:#111}a{color:#111}a:visited{color:#444}li{margin-bottom:0.5rem}header{text-align:center;margin-bottom:2rem}header h1{font-size:1.5rem;border:none;padding:0}header .evil{font-size:0.7rem;color:#111}footer{margin-top:1rem;border:1px dashed;padding:0.5rem;font-size:80%}h1,h2,h3,h4,h5,h6{font-weight:normal;font-size:1.2rem;line-height:1.3;margin-bottom:1rem;padding:0.5rem;border:1px dashed}h1{font-size:1.5rem}h2{font-size:1.3rem}article .header{font-size:0.9rem;font-style:italic;color:#444}article .footer{font-size:0.9rem;margin-top:2rem;padding-top:1rem}.post-date{font-size:0.7rem;color:#444}header a{color:#111;text-decoration:none}header a:visited{color:#111}.toc ul{list-style-type:none}pre{background-color:#f6f8ff;padding-left:1em;padding-right:1em;padding-top:0.5em;padding-bottom:0.5em;border-radius:0.5em}.paper-title{font-style:italic}.paper-links{font-size:70%}.award{font-weight:bold}table.sourceCode,tr.sourceCode,td.lineNumbers,td.sourceCode,table.sourceCode pre{margin:0;padding:0;border:0;vertical-align:baseline;border:none}td.lineNumbers{border-right:1px solid #AAAAAA;text-align:right;color:#AAAAAA;padding-right:5px;padding-left:5px}td.sourceCode{padding-left:5px}.sourceCode span.kw{color:#007020;font-weight:bold}.sourceCode span.dt{color:#902000}.sourceCode span.dv{color:#40a070}.sourceCode span.bn{color:#40a070}.sourceCode span.fl{color:#40a070}.sourceCode span.ch{color:#4070a0}.sourceCode span.st{color:#4070a0}.sourceCode span.co{color:#60a0b0;font-style:italic}.sourceCode span.ot{color:#007020}.sourceCode span.al{color:red;font-weight:bold}.sourceCode span.fu{color:#06287e}.sourceCode span.re{}.sourceCode span.er{color:red;font-weight:bold}pre.Agda a.Comment{color:#B22222}pre.Agda a.Keyword{color:#CD6600}pre.Agda a.String{color:#B22222}pre.Agda a.Number{color:#A020F0}pre.Agda a.Symbol{color:#404040}pre.Agda a.PrimitiveType{color:#0000CD}pre.Agda a.Operator{}pre.Agda a.Bound{color:black}pre.Agda a.InductiveConstructor{color:#008B00}pre.Agda a.CoinductiveConstructor{color:#8B7500}pre.Agda a.Datatype{color:#0000CD}pre.Agda a.Field{color:#EE1289}pre.Agda a.Function{color:#0000CD}pre.Agda a.Module{color:#A020F0}pre.Agda a.Postulate{color:#0000CD}pre.Agda a.Primitive{color:#0000CD}pre.Agda a.Record{color:#0000CD}pre.Agda a.DottedPattern{}pre.Agda a.UnsolvedMeta{color:black;background:yellow}pre.Agda a.UnsolvedConstraint{color:black;background:yellow}pre.Agda a.TerminationProblem{color:black;background:#FFA07A}pre.Agda a.IncompletePattern{color:black;background:#F5DEB3}pre.Agda a.Error{color:red;text-decoration:underline}pre.Agda a.TypeChecks{color:black;background:#ADD8E6}pre.Agda a{text-decoration:none}pre.Agda a[href]:hover{background-color:#B4EEB4}