diff --git a/.gitignore b/.gitignore index d80cf81d..acb793a2 100644 --- a/.gitignore +++ b/.gitignore @@ -38,3 +38,4 @@ docs/_includes/sorries.md *.synctex.gz *.synctex.gz(busy) *.pdfsync +*.pdf diff --git a/Notes/hott0.typ b/Notes/hott0.typ new file mode 100644 index 00000000..c7467392 --- /dev/null +++ b/Notes/hott0.typ @@ -0,0 +1,403 @@ +#import "prooftree.typ": prooftree, axiom, rule +#import "prelude.typ": * + +#show: template + +#let box_size = 8em + +We present #hott0 as an explicit substitution calculus. + +== Raw syntax +#v(1em) // TODO why is the spacing so tight by default + +$"(de Bruijn index)" i &∈ ℕ \ +"(type)" A,B ::=& U ∣ "El" t ∣ ∏_A B ∣ ∑_A B ∣ "Id"(u_0,u_1) ∣ A[σ] \ +"(term)" t,u ::=& bold(v)_i ∣ Π_t u ∣ Σ_t u ∣ "I "_t (u_0, u_1) \ + & ∣ λ_A t ∣ t#sp u ∣ ⟨ t , u ⟩_B ∣ "fst" t ∣ "snd" t \ + & ∣ "refl"_t ∣ "J"_A t ∣ t[σ] \ +"(context)" Θ,Δ,Γ ::=& · ∣ Γ.A \ +"(substitution)" σ,ρ ::=& id_Γ ∣ σ ∘ ρ ∣ ↑_A ∣ σ.t$ + +== Inference rules + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($⊢ Γ "ctx"$)), + $ prooftree(#rule($⊢ · "ctx"$, n: 0)) + + prooftree( + #axiom($Γ ⊢ A "type"$), + #rule($⊢ Γ.A "ctx"$)) + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($σ : Δ ⟶ Γ$)), + $ prooftree( + #axiom($⊢ Γ "ctx"$), + #rule($id_Γ : Γ ⟶ Γ$)) + + prooftree( + #axiom($ρ : Θ ⟶ Δ$), + #axiom($σ : Δ ⟶ Γ$), + #rule($σ∘ρ : Θ ⟶ Γ$, n: 2)) \ \ + + prooftree( + #axiom($Γ ⊢ A "type"$), + #rule($↑_A : Γ.A ⟶ Γ$)) + + prooftree( + #axiom($σ : Δ ⟶ Γ$), + #axiom($Δ ⊢ t : A[σ]$), + #rule($σ.t : Δ ⟶ Γ.A$, n: 2)) + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($σ ≡ ρ : Δ ⟶ Γ$)), + $ prooftree( + #axiom($σ : Δ ⟶ Γ$), + #axiom($Δ ⊢ t : A[σ]$), + #rule($↑_A∘σ.t ≡ σ : Δ ⟶ Γ$, n: 2)) + + \ \ + + prooftree( + #axiom($ρ : Θ ⟶ Δ$), + #axiom($σ : Δ ⟶ Γ$), + #axiom($Θ ⊢ t : A[σ∘ρ]$), + #rule($(σ∘ρ).t ≡ ... : Θ ⟶ Γ$, n: 3)) + + "(+ axioms of a category.)" + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($Γ ⊢ A "type"$)), + $ prooftree(#rule($Γ ⊢ U "type"$, n: 0)) + + prooftree( + #axiom($Γ ⊢ t : U$), + #rule($Γ ⊢ "El" t "type"$)) + + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($Γ.A ⊢ B "type"$), + #rule($Γ ⊢ ∏_A B "type"$, n: 2)) + + \ \ + + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($Γ.A ⊢ B "type"$), + #rule($Γ ⊢ ∑_A B "type"$, n: 2)) + + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($Γ ⊢ u_0 : A$), + #axiom($Γ ⊢ u_1 : A$), + #rule($ Γ ⊢ "Id"(u_0,u_1) "type"$, n: 3)) + + \ \ + + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($σ : Δ ⟶ Γ$), + #rule($Δ ⊢ A[σ] "type"$, n: 2)) + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($Γ ⊢ A ≡ B "type"$)), + $ + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ."El" t ⊢ u : U$), + #rule($Γ ⊢ "El" (Π_t u) ≡ ∏_("El" t)"El" u "type"$, n: 2)) + + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ."El" t ⊢ u : U$), + #rule($Γ ⊢ "El" (Σ_t u) ≡ ∑_("El" t)"El" u "type"$, n: 2)) + + \ \ + + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ ⊢ u_0 : "El" t$), + #axiom($Γ ⊢ u_1 : "El" t$), + #rule($Γ ⊢ "El" ("I "_t (u_0, u_1)) ≡ "Id"(u_0, u_1)$, n: 3)) + + "(+ substitution naturalities.)" + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($Γ ⊢ t : A$)), + $ + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ."El" t ⊢ u : U$), + #rule($Γ ⊢ Π_t u : U$, n: 2)) + + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ."El" t ⊢ u : U$), + #rule($Γ ⊢ Σ_t u : U$, n: 2)) + + \ \ + + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ ⊢ u_0 : "El" t$), + #axiom($Γ ⊢ u_1 : "El" t$), + #rule($Γ ⊢ "I "_t (u_0, u_1) : U$, n: 3)) + + \ \ + + prooftree( + #axiom($Γ.A ⊢ t : B$), + #rule($Γ ⊢ λ_A t : ∏_A B$)) + + prooftree( + #axiom($Γ ⊢ t : ∏_A B$), + #axiom($Γ ⊢ u : A$), + #rule($Γ ⊢ t#sp u : B[id_Γ.u]$, n: 2)) + + \ \ + + prooftree( + #axiom($Γ ⊢ t : A$), + #axiom($Γ ⊢ u : B[id_Γ.t]$), + #rule($Γ ⊢ ⟨ t , u ⟩_B : ∑_A B$, n: 2)) + + prooftree( + #axiom($Γ ⊢ t : ∑_A B$), + #rule($Γ ⊢ "fst" t : A$)) + + prooftree( + #axiom($Γ ⊢ t : ∑_A B$), + #rule($Γ ⊢ "snd" t : B[id_Γ."fst" t]$)) + + \ \ + + prooftree( + #axiom($Γ ⊢ t : A$), + #rule($Γ ⊢ "refl"_t : "Id"(t, t)$) + ) + + prooftree( + #axiom($Γ.A.A[↑_A]."Id"(bold(v)_1, bold(v)_0) ⊢ B "type"$), + #axiom($Γ.A ⊢ t : B[id_(Γ.A) . v_0 . "refl"_v_0]$), + #rule($Γ.A.A[↑_A]."Id"(bold(v)_1, bold(v)_0) ⊢ J_B (t) : B$, n: 2) + ) + + \ \ + + prooftree( + #axiom($Γ ⊢ A "type"$), + #rule($Γ.A ⊢ bold(v)_0 : A[↑_A]$)) + + prooftree( + #axiom($Γ ⊢ t : A$), + #axiom($σ : Δ ⟶ Γ$), + #rule($Δ ⊢ t[σ] : A[σ]$, n: 2)) + \ \ + $ +)) + +#figure(grid( + columns: (box_size, 1fr), + align(left, gbox($Γ ⊢ t ≡ u : A$)), + $ "(TODO: standard)" + $ +)) + + +== Nondepenent functions and binary products + + + $ + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($Γ ⊢ B "type"$), + #rule($Γ ⊢ A × B ≜ ∑_A B[↑_A]$, n: 2)) + + #h(1cm) + + prooftree( + #axiom($Γ ⊢ A "type"$), + #axiom($Γ ⊢ B "type"$), + #rule($Γ ⊢ A → B ≜ ∏_A B[↑_A]$, n: 2)) + $ + + $ + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ ⊢ u : U$), + #rule($Γ ⊢ t × u ≜ Σ_t u[↑_("El" t)]$, n: 2)) + + #h(1cm) + + prooftree( + #axiom($Γ ⊢ t : U$), + #axiom($Γ ⊢ u : U$), + #rule($Γ ⊢ t → u ≜ Π_t u[↑_("El" t)]$, n: 2)) + $ + +== Univalence + +In the following we will use $[↑^?]$ to denote a series of weakening substitutions, +which will be clear from context. + +Univalence will be a term of the (merely propositional) type +$ Γ.U.U[↑] ⊢ "IsBigEquiv"[id_( Γ.U.U[↑] ) . "IdToEquiv"] "type" $ +Here $"IsBigEquiv"$ and its components $"BigLinv"$ and $"BigRinv"$ (defined later) +are shorthand for longer type expressions, +whereas "IdToEquiv" is a term expression. +In order to write the type expressions as shorthands internal to the type theory +it is necessary and sufficient to have a second, +larger universe containing $"U"$ as a term. + +Supposing that $Γ ⊢ A "type"$ and $Γ ⊢ B "type"$ we define the shorthands + +$ Γ.A → B ⊢ + "BigLinv"_(A,B) ≜ ∑_((B → A)[↑^?]) ∏_(A[↑^?]) + "Id"( bold(v_1)(bold(v_2) #sp bold(v_0)) , bold(v_0) ) $ + +$ Γ.A → B ⊢ + "BigRinv"_(A,B) ≜ ∑_((B → A)[↑^?]) ∏_(B[↑^?]) + "Id"( bold(v_2)(bold(v_1) #sp bold(v_0)) , bold(v_0) ) $ + +$ Γ.A → B ⊢ "IsBigEquiv"_(A,B) ≜ "BigLinv"_(A,B) × "BigRinv"_(A,B) $ + +We can verify that + +$ + Γ.A → B ⊢ "BigLinv"_(A,B) "type" + #h(1cm) + Γ.A → B ⊢ "BigRinv"_(A,B) "type" + #h(1cm) + Γ.A → B ⊢ "IsBigEquiv"_(A,B) "type" +$ + +There are also versions of these bounded by the universe $"U"$. +// Supposing that we have two codes for small types +// $Γ ⊢ u_A : U$ and $Γ ⊢ u_B : U$ + +#let easy(x) = text(fill: blue, $#x$) + +// $ Γ."El"(u_A → u_B) ⊢ "Linv" ≜ Σ_((u_B → u_A)[↑^?]) Π_(u_A [↑^?]) "I "_(u_A [↑^?]) +// ( bold(v_1)(bold(v_2) #sp bold(v_0)) , bold(v_0) ) : U[↑^?] $ + +$ Γ.U.U[↑]."El"(bold(v_0) → bold(v_1)) ⊢ + "Linv" ≜ Σ_(bold(v_1) → bold(v_2)) Π_(bold(v_3)) + "I "_(bold(v_4))( bold(v_1)(bold(v_2) #sp bold(v_0)) , bold(v_0) ) : U[↑^?] $ +$ easy(Γ.a:U.b:U.f:"El"(a → b) ⊢ + "Linv" ≜ Σ_(g:"El" (b → a)) Π_(x: "El" a) + "I "_a ( g(f #sp x) , x ) : U ) $ + +$ Γ.U.U[↑]."El"(bold(v_0) → bold(v_1)) ⊢ + "Rinv" ≜ Σ_(bold(v_1) → bold(v_2)) Π_(bold(v_3)) + "I "_(bold(v_4))( bold(v_1)(bold(v_2) #sp bold(v_0)) , bold(v_0) ) : U[↑^?] $ +$ easy(Γ.a:U.b:U.f:"El"(a → b) ⊢ + "Rinv" ≜ Σ_(g:"El" (b → a)) Π_(x: "El" b) "I "_b ( f(g #sp x) , x ) : U) $ + +// $ Γ."El"(u_A → u_B) ⊢ "Rinv" ≜ Σ_((u_B → u_A)[↑^?]) Π_(u_B[↑^?]) +// "I "_(u_B) ( bold(v_2)(bold(v_1) #sp bold(v_0)) , bold(v_0) ) $ + +$ Γ.U.U[↑]."El"(bold(v_0) → bold(v_1)) ⊢ "IsEquiv" ≜ "Linv" × "Rinv" : U[↑^?] $ + +$ Γ.U.U[↑] ⊢ "Equiv" ≜ Σ_(bold(v_1) → bold(v_0)) "IsEquiv" : U[↑^?] $ + +When we define +$Γ.U.U[↑] ⊢ "IdToEquiv" : "Id"(bold(v_1), bold(v_0)) → "Equiv"$, +we see the necessesity of defining both big and small equivalences; +given $u_0 , u_1 : U$ we do not have $"Id"(u_0, u_1) : U$. + +The underlying function in our equivalence transports along the given identity +$ Γ.U.U[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ "IdToFun" ≜ + J_("El"(bold(v_2) → bold(v_1))) (λ_("El"bold(v_0)) v_0) : "El"(bold(v_2) → bold(v_1)) $ + +$ easy(Γ.a:U.b:U."Id"(a, b) ⊢ "IdToFun" ≜ J_("El"(a → b)) id_("El" a) : "El"(a → b)) $ +// $ Γ.U.U[↑] ⊢ "IdToFun" ≜ +// λ_("Id"(bold(v_1) , bold(v_0))) +// ( J_("El"(bold(v_2) → bold(v_1))) (λ_("El"bold(v_0)) v_0) ) : +// "Id"(bold(v_1) , bold(v_0)) → "El"(bold(v_2) → bold(v_1)) $ + +// $ easy(Γ.a:U.b:U ⊢ "IdToFun" ≜ +// λ_("Id"(a, b)) ( J_("El"(a → b)) id_("El" a) ) : "El"(a → b)) $ + +Identity is symmetrical, which we use to construct the inverse in the equivalence. +$ Γ.A.A[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ + "sym"_A ≜ J_("Id"(bold(v_1), bold(v_2))) "refl"_(bold(v_0)) : "Id"(bold(v_1), bold(v_2)) $ + +$ easy(Γ.x:A.y:A."Id"(x, y) ⊢ "sym"_A ≜ J_("Id"(y,x)) "refl"_x : "Id"(y,x)) $ + +The inverse of the equivalence +$ Γ.U.U[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ "IdToInv" ≜ + "IdToFun"[id_Γ.bold(v_1).bold(v_2)."sym"_U] : "El"(bold(v_1) → bold(v_2)) $ + +$ easy(Γ.a:U.b:U."Id"(a, b) ⊢ "IdToInv" ≜ "IdToFun"[id_Γ.b.a."sym"_U] : "El"(b → a)) $ + +That it is a left inverse and a right inverse can be proven with path induction, +where the diagonal case is an equality that holds definitionally, +by the computation rule for $J$. +$ Γ.U.U[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ "LinvIdToFun" ≜ ⟨ "IdToInv", + J_("El"(Π_(bold(v_2)) "I "_(bold(v_3))( "IdToInv"[↑]("IdToFun"[↑] #sp bold(v_0)) , bold(v_0) ))) + (λ_("El" bold(v_0)) "refl"_(bold(v_0))) + ⟩ $ +$ : "Linv"[↑_("Id"(bold(v_1), bold(v_0))) . "IdToFun"[↑]] $ + +$ Γ.U.U[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ "RinvIdToFun" ≜ ⟨ "IdToInv", + J_("El"(Π_(bold(v_1)) "I "_(bold(v_2))( "IdToInv"[↑]("IdToFun"[↑] #sp bold(v_0)) , bold(v_0) ))) + (λ_("El" bold(v_0)) "refl"_(bold(v_0))) + ⟩ $ +$ : "Rinv"[↑_("Id"(bold(v_1), bold(v_0))) . "IdToFun"[↑]] $ + +Now we have all the components for defining $"IdToEquiv"$ + +$ Γ.U.U[↑]."Id"(bold(v_1) , bold(v_0)) ⊢ "IsEquivIdToFun" ≜ ⟨ "IdToFun", + ⟨ + "LinvIdToFun", + "RinvIdToFun" + ⟩ + ⟩ $ +$ : "IsEquiv"[↑_("Id"(bold(v_1), bold(v_0))) . "IdToFun"[↑]] $ + + +$ Γ.U.U[↑] ⊢ "IdToEquiv" ≜ λ_("Id"(bold(v_1), bold(v_0))) ⟨ "IdToFun" , "IsEquivIdToFun" ⟩ : "Id"(bold(v_1), bold(v_0)) → "Equiv" $ + +// $ easy(Γ.U.U[↑] ⊢ "IdToEquiv" ≜ λ_("Id"(bold(v_1), bold(v_0))) ⟨ "IdToFun" , "IsEquivIdToFun" ⟩ : "Id"(bold(v_1), bold(v_0)) → "Equiv") $ + +Finally, the univalence axiom states + +$ + prooftree( + #rule($Γ.U.U[↑] ⊢ "ua" : "IsBigEquiv"[id_( Γ.U.U[↑] ) . "IdToEquiv"]$, n: 0) +) + +$ + +== Uniqueness of Identity Principle + +In the groupoid model of HoTT, +we could take the universe $"U"$ to be all small discrete groupoids, +i.e. small sets. +In lean, these would satisfy the uniqueness of identity principle (UIP). + +$ + prooftree( + #axiom($Γ ⊢ u_A : U$), + #axiom($Γ ⊢ t_0 : "El" u_A$), + #axiom($Γ ⊢ t_1 : "El" u_A$), + #axiom($Γ ⊢ p : "Id"(t_0,t_1)$), + #axiom($Γ ⊢ q : "Id"(t_0,t_1)$), + #rule($Γ ⊢ p ≡ q : "Id"(t_0,t_1)$,n:5) +) +$ diff --git a/Notes/prelude.typ b/Notes/prelude.typ new file mode 100644 index 00000000..daa78d72 --- /dev/null +++ b/Notes/prelude.typ @@ -0,0 +1,43 @@ +#let template(doc) = [ + // Numbering and styling for headings + #set heading(numbering: "1.") + #show heading.where(level: 3): set heading(outlined: false) + #show heading.where(level: 4): set heading(outlined: false) + #show heading: it => { + if it.level < 3 { it } + else { + if it.numbering != none [ + #counter(heading).display("1.") #it.body. + ] else [ + #it.body. + ] + } + } + + // Don't number equations + #set math.equation(numbering: none) + + // Improve behaviour of some math symbols + #show math.equation: it => { + show sym.arrow.t: math.class.with("unary") + show sym.arrow.b: math.class.with("unary") + show sym.arrow.r.double: math.class.with("binary") + show sym.bot: math.class.with("normal") + show sym.tack: math.scripts + show sym.arrow.r: math.scripts + show sym.arrow.r.twohead: math.scripts + show sym.eq.triple: math.scripts + show sym.arrow.r.long: math.scripts + show sym.eq: math.scripts + it + } + + #doc +] + +// A nice box +#let gbox(content) = box(stroke: black, inset: 6pt, baseline: 6pt, content) + +#let hott0 = $"HoTT"_0$ + +#let sp = h(.3em) diff --git a/Notes/prooftree.typ b/Notes/prooftree.typ new file mode 100644 index 00000000..a03fb384 --- /dev/null +++ b/Notes/prooftree.typ @@ -0,0 +1,357 @@ +#let prooftree( + spacing: ( + horizontal: 1em, + vertical: 0.5em, + lateral: 0.5em, + ), + label: ( + // TODO: split offset into horizontal and vertical + offset: -0.1em, + side: right, + padding: 0.2em, + ), + line-stroke: 0.5pt, + ..rules +) = { + // Check the types of the parameters. + assert( + type(spacing) == "dictionary", + message: "The value `" + repr(spacing) + "` of the `spacing` argument was expected" + + "to have type `dictionary` but instead had type `" + type(spacing) + "`." + ) + assert( + type(label) == "dictionary", + message: "The value `" + repr(label) + "` of the `label` argument was expected" + + "to have type `dictionary` but instead had type `" + type(label) + "`." + ) + assert( + type(line-stroke) == "length", + message: "The value `" + repr(line-stroke) + "` of the `line-stroke` argument was expected" + + "to have type `length` but instead had type `" + type(line-stroke) + "`." +) + + // Check validity of `spacing`'s keys. + for (key, value) in spacing { + if key not in ("horizontal", "vertical", "lateral", "h", "v", "l") { + panic("The key `" + key + "` in the `spacing` argument `" + repr(spacing) + "` was not expected.") + } + if type(value) != "length" { + panic( + "The value `" + repr(value) + "` of the key `" + key + "` in the `spacing` argument `" + repr(spacing) + + "` was expected to have type `length` but instead had type `" + type(value) + "`." + ) + } + } + + // Check exclusivity of `spacing`'s keys. + let mutually_exclusive(key1, key2, keys) = { + assert( + key1 not in keys or key2 not in keys, + message: "The keys `" + key1 + "` and `" + key2 + "` in the `spacing` argument `" + + repr(spacing) + "` are mutually exclusive." + ) + } + mutually_exclusive("horizontal", "h", spacing.keys()) + mutually_exclusive("vertical", "v", spacing.keys()) + mutually_exclusive("lateral", "l", spacing.keys()) + + // Check validity of `label`'s keys. + let expected = ("offset": "length", "side": "alignment", "padding": "length") + for (key, value) in label { + if key not in expected { + panic("The key `" + key + "` in the `label` argument `" + repr(label) + "` was not expected.") + } + if type(value) != expected.at(key) { + panic( + "The value `" + repr(value) + "` of the key `" + key + "` in the `label` argument `" + repr(label) + + "` was expected to have type `" + type.at(key) + "` but instead had type `" + type(value) + "`." + ) + } + } + if "side" in label { + assert( + label.side == left or label.side == right, + message: "The value for the key `side` in the argument `label` can only be either " + + "`left` (default) or `right`, but instead was `" + repr(label.side) + "`." + ) + } + + // Check basic validity of `rules`. + if rules.pos().len() == 0 { + panic("The `rules` argument cannot be empty.") + } + + let settings = ( + spacing: ( + horizontal: spacing.at("horizontal", default: spacing.at("h", default: 1.5em)), + vertical: spacing.at("vertical", default: spacing.at("v", default: 0.5em)), + lateral: spacing.at("lateral", default: spacing.at("l", default: 0.5em)), + ), + label: ( + offset: label.at("offset", default: -0.1em), + side: label.at("side", default: left), + padding: label.at("padding", default: 0.2em), + ), + line-stroke: line-stroke, + ) + + // Draw the rules in a stack-based evaluation order. + style(styles => { + let stack = () + + for rule in rules.pos() { + let to_pop = rule.__prooftree_to_pop + let rule_func = rule.__prooftree_rule_func + + assert( + to_pop <= stack.len(), + message: "The rule `" + repr(rule.__prooftree_raw) + "` was expecting at least " + + str(to_pop) + " rules in the stack, but only " + str(stack.len()) + " were present." + ) + + let elem = rule_func( + settings, + styles, + stack.slice(stack.len() - to_pop) + ) + + stack = stack.slice(0, stack.len() - to_pop) + stack.push(elem) + } + + assert( + stack.len() == 1, + message: "Some rule remained unmatched: " + str(stack.len()) + " roots were found but only 1 was expected." + ) + + set align(start) + set box(inset: 0pt, outset: 0pt) + + stack.pop().body + }) +} + +#let axiom(label: none, body) = { + // Check the type of `label`. + assert( + type(label) in ("string", "content", "none"), + message: "The type of the `label` argument `" + repr(label) + "` was expected to be " + + "`none`, `string` or `content` but was instead `" + type(label) + "`." + ) + + // TODO: allow the label to be aligned on left, right or center (default and current). + + ( + __prooftree_raw: body, + __prooftree_to_pop: 0, + __prooftree_rule_func: (settings, styles, children) => { + let body = box(body, inset: (x: settings.spacing.lateral)) + // let body = body + if label != none { + // Labels stack on top of axioms + body = stack( + dir: ttb, + spacing: 1.5 * settings.spacing.vertical, + align(center, label), + body + ) + } + + return ( + body: body, + label_wleft: 0pt, + label_wright: 0pt, + wleft: 0pt, + wright: 0pt, + ) + } + ) +} + +#let rule( + n: 1, + label: none, + root +) = { + // Check validity of the `n` parameter + assert( + type(n) == "integer", + message: "The type of the `n` argument `" + repr(n) + "` was expected to be " + + "`integer` but was instead `" + type(n) + "`." + ) + + // Check the type of `label`. + assert( + type(label) in ("string", "dictionary", "content", "none"), + message: "The type of the `label` argument `" + repr(label) + "` was expected to be " + + "`none`, `string`, `content` or `dictionary` but was instead `" + type(label) + "`." + ) + // If the type of `label` was string then it's good, otherwise we need to check its keys. + if type(label) == "dictionary" { + for (key, value) in label { + // TODO: maybe consider allowing `top`, `top-left` and `top-right` if `rule(n: 0)` gets changed. + if key not in ("left", "right") { + panic("The key `" + key + "` in the `label` argument `" + repr(label) + "` was not expected.") + } + if type(value) not in ("string", "content") { + panic( + "The value `" + repr(value) + "` of the key `" + key + "` in the `label` argument `" + repr(label) + + "` was expected to have type `string` or `content` but instead had type `" + type(value) + "`." + ) + } + } + } + + ( + __prooftree_raw: root, + __prooftree_to_pop: n, + __prooftree_rule_func: (settings, styles, children) => { + let width(it) = measure(it, styles).width + let height(it) = measure(it, styles).height + let maxl(..lengths) = width( + for length in lengths.pos() { + line(length: length) + } + ) + let gtl(l1, l2) = maxl(l1, l2) != l2 + let minl(l1, l2) = if gtl(l1, l2) { l2 } else { l1 } + + let root = [ #h(settings.spacing.lateral) #root #h(settings.spacing.lateral) ] + + // Get some values from the children, or 0pt if n == 0 + let ( + children_wleft, + children_label_wleft, + children_wright, + children_label_wright + ) = (0pt, 0pt, 0pt, 0pt) + if n != 0 { + children_wleft = children.first().wleft + children_label_wleft = children.first().label_wleft + children_wright = children.last().wright + children_label_wright = children.last().label_wright + } + + // Map the children to a single block + let branches = children.map(c => box(c.body)).join(h(settings.spacing.horizontal)) + + // Calculate the offsets of the "inner" branches, i.e. ignoring branches' labels + let wbranches_nolabel = width(branches) - children_label_wleft - children_label_wright + let ibranches_offset = maxl(0pt, width(root) - wbranches_nolabel) / 2 + + // Compute the start, end and length of the line to satisfy the "inner" branches + let ib_line_start = ibranches_offset + children_wleft + let ib_line_end = ibranches_offset + wbranches_nolabel - children_wright + let ib_line_len = ib_line_end - ib_line_start + + // Pad the line length to satisfy the root too + let line_len = maxl(ib_line_len, width(root)) + + // Adjust the line start to account for the root padding + let line_start = if gtl(ib_line_len, width(root)) { + // No root padding + ib_line_start + } else if gtl(width(root), wbranches_nolabel) { + // The "inner" branches are too tight + 0pt + } else { + // Weird, situation, we have `wbranches_nolabel > width(root) > ib_line_len` + // The line should be adjusted so that it fits kinda in the middle + // TODO: maybe this should also consider labels? + let min_left = maxl(0pt, ib_line_end - line_len) + let max_right = minl(maxl(wbranches_nolabel, width(root)), ib_line_start + line_len) + (max_right + min_left) / 2 - line_len / 2 + } + + // Finish computing the offsets by considering the ignored left branches label + let branches_offset = maxl(0pt, ibranches_offset - children_label_wleft) + let line_start = line_start + (branches_offset + children_label_wleft - ibranches_offset) + let root_offset = line_start + (line_len - width(root)) / 2 + + // Compute body without the label. + // This is needed later to calculate the sizes when placing the new labels. + let body_nolabel = stack( + dir: ttb, + spacing: settings.spacing.vertical, + box(inset: (left: branches_offset), branches), + line(start: (line_start, 0pt), length: line_len, stroke: settings.line-stroke), + box(inset: (left: root_offset), root), + ) + + // Normalize label given the default value in the `prooftree` function. + let label = label + if type(label) == "none" { + label = ( + left: none, + right: none + ) + } + if type(label) in ("string", "content") { + label = ( + left: if settings.label.side == left { label } else { none }, + right: if settings.label.side == right { label } else { none } + ) + } + label = ( + left: label.at("left", default: none), + right: label.at("right", default: none), + ) + + // Pad the labels to separate them from the rule + let left_label = box(inset: (right: settings.label.padding), label.left) + let right_label = box(inset: (left: settings.label.padding), label.right) + + // Compute extra space the left label might need + let new_left_space = maxl(0pt, width(left_label) - line_start) + let left_label_width_offset = maxl(0pt, line_start - width(left_label)) + + // Compute the width offset of the right label + let right_label_width_offset = new_left_space + line_start + line_len + + // Compute the final width + let final_width = maxl( + right_label_width_offset + width(right_label), + new_left_space + width(body_nolabel) + ) + + // Place the label on top of the rest. + // Note that this needs to fix the final dimensions in order to use `place`. + let body = box(width: final_width, height: height(body_nolabel))[ + #set block(spacing: 0pt) + #box(inset: (left: new_left_space), body_nolabel) + #place( + bottom + left, + dx: left_label_width_offset, + dy: settings.label.offset, + box(height: 2 * (height(root) + settings.spacing.vertical), align(horizon, left_label)) + ) + #place( + bottom + left, + dx: right_label_width_offset, + dy: settings.label.offset, + box(height: 2 * (height(root) + settings.spacing.vertical), align(horizon, right_label)) + ) + ] + + // Compute the final sizes for the next rule + let label_wleft = minl( + new_left_space + branches_offset + children_label_wleft, + left_label_width_offset + width(left_label) + ) + let label_wright = minl( + children_label_wright + (final_width - branches_offset - width(branches)), + final_width - right_label_width_offset + ) + let wleft = (new_left_space + root_offset) - label_wleft + let wright = width(body) - new_left_space - root_offset - width(root) - label_wright + + ( + body: body, + label_wleft: label_wleft, + label_wright: label_wright, + wleft: wleft, + wright: wright, + ) + } + ) +}