chore: small fixes to text of 1Lab.Path

[ahubers]

(First of all, huge fan of 1Lab! Thanks for so many informative pages.)

Description

• small typo fix (line 874).
• I changed the typing rules on https://1lab.dev/1Lab.Path.html

Justifying my changes

I changed the rule:

$$ \frac{ \Gamma, i : \mathbb{I} \vdash e : A \quad \Gamma \vdash e(\rm{i0}) = a : A(\rm{i0}) \quad \Gamma \vdash e(\rm{i1}) = b : A(\rm{i1}) \quad }{ \Gamma \vdash (\lambda {i}.{e}) : \rm{PathP}~ {A}~ {a}~ {b} } $$

to:

$$ \frac{ \Gamma, i : \mathbb{I} \vdash e : A(i) \quad \Gamma \vdash e[\rm{i0} / i] = a : A(\rm{i0}) \quad \Gamma \vdash e(\rm{i1} / i] = b : A(\rm{i1}) \quad }{ \Gamma \vdash (\lambda {i}.{e}) : \rm{PathP}~ {A}~ {a}~ {b} } $$

• The introduction rule for PathP has a $$\lambda$$-binding, and the assumption $$\Gamma, i : I \vdash e : A$$ implies that $$i$$ appears freely in $$e$$. So we need to substitute $$i0$$ and $$i1$$ in the body of $$e$$.
• Also, we can't have $$\Gamma, i : I \vdash e : A$$ as $$A$$ is not a sort; I've changed the text to read $$\Gamma, i : I \vdash e : A(i)$$.

[Lavenza]

Pull request preview

Changed pages

• 1Lab.Path (± 4)