type-theory/thesis/style.typ
2025-02-18 18:23:57 -06:00

115 lines
No EOL
3.3 KiB
Typst

#import "@preview/cetz:0.3.1" as cetz: canvas, draw
#import "@preview/ctheorems:1.1.3": *
#let template(title: "", content) = {
set text(
// font: "New Computer Modern Math",
size: 12pt,
)
set page(
"us-letter",
margin: 1in,
)
set par(
// leading: 1.3em,
// spacing: 2.4em,
// first-line-indent: 1.8em,
justify: true,
)
set heading(
numbering: "1.1",
)
show: thmrules
show link: body => underline(text(fill: rgb("#009900"), body))
// show heading: set block(above: 1.4em, below: 1em)
align(center)[
#heading(outlined: false, numbering: none, text(size: 2em)[#title])
]
outline(title: [Table of Contents], indent: true, depth: 2)
outline(title: [Table of Figures], indent: true, depth: 2, target: figure)
page(
numbering: "1", // TODO: Remove
content,
)
heading(outlined: false, numbering: none)[References]
bibliography("main.bib", title: none)
}
#let TODO(c) = [#text(fill: red)[*TODO:* #c]]
#let agdaCubicalLink(s) = link("https://github.com/agda/cubical/blob/2f085f5675066c0e1708752587ae788c036ade87/" + s.split(".").join("/") + ".agda", raw(s))
// ctheorems
#let theorem = thmbox("thm", "Theorem", fill: rgb("#eeffff"))
#let definition = thmbox("thm", "Definition", fill: rgb("#eeeeff"))
#let example = thmbox("thm", "Example", fill: rgb("#eeffee"))
#let notation = thmbox("thm", "Notation", fill: rgb("#ffeeee"))
#let axiom = thmbox("thm", "Axiom", fill: rgb("#ffeeee"))
#let prf = thmproof("thm", "Proof")
// #let theorem = thmbox("theorem", "Theorem", fill: rgb("#eeffee"))
// #let corollary = thmplain(
// "corollary",
// "Corollary",
// base: "theorem",
// titlefmt: strong
// )
// #let definition = thmbox("definition", "Definition")
// #let axiom = thmplain("axiom", "Axiom")
// #let example = thmplain("example", "Example").with(numbering: none)
#let proof = thmproof("proof", "Proof")
#let point(pos, paint: black, ..args) = cetz.draw.circle(pos, radius: 0.08, fill: paint, stroke: paint, ..args)
// Notation
#let emptyType = $bot$
#let lam(x, a) = $lambda #x op(.) #a$
#let arro(..a) = $#a.pos().join($op(arrow)$)$
#let judgCtx(a) = $#a sans("ctx")$
#let isTyp(a, b) = $#a op(:) #b$
#let judgTyp(G, a, A) = $#G tack.r isTyp(#a, #A)$
#let propEqSym = $equiv$
#let propEq(a, b) = $#a #propEqSym #b$
#let propEqTy(a, b, A) = $#a op(#propEqSym)_(#A) #b$
#let refl = $sans("refl")$
#let idfun = $sans("id")$
#let eqv(a, b) = $#a tilde.eq #b$
#let defEq(a, b) = $#a :equiv #b$
#let judgEqTyp(G, a, b, A) = $#G tack.r isTyp(#a equiv #b, #A)$
#let imSym = link(<image>)[$sans("Im")$]
#let imOf(f) = $#imSym\(f)$
#let kerOf(f) = $sans("Ker")(#f)$
#let ind = $sans("ind")$
#let ap = $sans("ap")$
#let apd = $sans("apd")$
#let ua = $sans("ua")$
#let uaEqv = $sans("uaEqv")$
#let isEquiv = $sans("isEquiv")$
#let typ = $sans("Type")$
#let abst(n, b) = $(#n) arrow.r.double #b$
#let typ0 = $typ_0$
#let BoolVec = $sans("BoolVec")$
#let Vec = $sans("Vec")$
#let unitType = link(<unitType>)[$bb(1)$]
#let tt = $sans("tt")$
#let boolType = link(<boolType>)[$sans("Bool")$]
#let bTrue = $sans("true")$
#let bFalse = $sans("false")$
#let neg = $sans("neg")$
#let negOf(A) = $not #A$
#let seg = $sans("seg")$
#let S1 = link(<circle>)[$S^1$]
#let base = $sans("base")$
#let loop = $sans("loop")$
#let AbGroup = $sans("AbGroup")$
#let hom(a, b) = $#a arrow.r.double #b$
#let homComp(a, b) = $#a op(circle.small) #b$