2
$\begingroup$

This question is based on the talks given by Mike Shulman on higher observational type theory (part 1, part 2, part 3).

In trying to understand the reduction rules of the calculus, I tried to work through some examples using the rules present on slide 7 in part 2 (I've copied in a screenshot below, and am assuming there's a missing $\Delta$ on the LHS for the dependent product/function case, but I could be wrong):

reduction rules

The below example gave me some trouble, however: It seems that the variable $x$ can 'escape' it's scope:

\begin{aligned} &Id_{Δ.((Π (x : A) (y : B\:x). C))}^δ(f, g)\\ ≡ &\Pi (u, v : A). \Pi(p: Id_{Δ.A}^δ (u, v)).\: (Id_{(Δ, x:A).(Π (y : B\:x). C)}^{δ, p} (f\: u, g\: v))\\ ≡ &\Pi (u, v : A) (p: Id_{Δ.A}^δ (u, v)) (m, n : B\: x) (q : Id_{(Δ, x:A).B}^{δ,p}(m, n)). Id_{(Δ, x:A, y:B).C}^{δ, p, q} (f\: u\: m, g\: v\: n) \end{aligned}

My question basically boils down to: what went wrong here? Am I misinterpreting the rules? Is there a typo on the slides?

Any help would be greatly appreciated.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ This is just a guess, but I suspect the rules should actually use something like $u : A[δ_l]$, where $δ_l$ is obtained from $δ$ by always choosing the left end point of the identities. Similarly $v$ would use a $δ_r$. I.E. an identity of functions actually turns into a function taking values from each endpoint, which only degenerates to $A$ (no substitutions) for both when it is not dependent on anything in the context. $\endgroup$
    – Dan Doel
    Commented Sep 27, 2023 at 14:26
  • $\begingroup$ Happy to see someone else made the same diagnosis as me! $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Sep 27, 2023 at 14:30
  • $\begingroup$ I think you can look at the agda development for the details. $\endgroup$
    – Trebor ♦
    Commented Sep 28, 2023 at 5:12

1 Answer 1

Reset to default
2
$\begingroup$

I would guess the issue comes from the $\Delta$ you assumed was missing. As far as I can tell, when living over a general telescope, already $$ Id_{Δ.(Π (x : A) B)}^δ(f, g) ≡ \Pi (u, v : A). \Pi(p: Id_{Δ.A}^δ (u, v)).(Id_{(Δ, x:A).B}^{δ, p} (f\: u, g\: v)) $$ is problematic. Indeed, the binder $(u,v : A)$ is not sensible, as $A$ lives over $\Delta$. Rather, you should have something like $$ Id_{Δ.(Π (x : A) B)}^δ(f, g) ≡ \Pi (u : A[δ_{L}]) (v : A[δ_{R}]). \Pi(p: Id_{Δ.A}^δ (u, v)).(Id_{(Δ, x:A).B}^{δ, p} (f\: u, g\: v)) $$ where $δ_{L} : \Delta$ is the list of left endpoints of the telescope of equalities $δ$, and similarly for $δ_{R}$.

If you repeat this, you'll get \begin{aligned} &Id_{Δ.((Π (x : A) (y : B\:x). C))}^δ(f, g)\\ ≡ &\Pi (u : A[δ_{L}]) (v : A[δ_{R}]) (p: Id_{Δ.A}^δ (u, v)).\: (Id_{(Δ, x:A).(Π (y : B\:x). C)}^{δ, p} (f\: u, g\: v))\\ ≡ &\Pi (u : A[δ_{L}]) (v : A[δ_{R}]) (p: Id_{Δ.A}^δ (u, v)) (m : B[δ_{L},u]) (n : B[δ_{R},v]) (q : Id_{(Δ, x:A).B}^{δ,p}(m, n)). Id_{(Δ, x:A, y:B).C}^{δ, p, q} (f\: u\: m, g\: v\: n) \end{aligned} (using that $(δ,p)_{L}$ is $(δ_{L},u)$ since $u$ is the left endpoint of $p$, and scoping is fine.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.