1
$\begingroup$

For example, in the proof of lemma 6.4.1 in the HoTT book, a function inductively defined over a function is simply applied on paths loop and refl, and then a path between loop and refl is used (presumably by congruence via f) to construct a path between f loop and f refl:

Suppose that loop = refl base. [...] with x : A and p : x = x, there is a function f : S1 → A defined by f(base) :≡ x and f(loop) := p, we have

p = f(loop) = f(refl base) = refl x.

But in a cubical setting, things are not so clear-cut. f(loop) is not well-typed, only f(loop i) is, for some i : I. But then that above proof becomes

p = <i> f (loop i) = <i> f (refl base i) = refl x

but doesn't that need some kind of "interval extensionality" in the middle step? What exactly is the justification of the middle step in cubical type theory? I can see how to prove ∀ i → f (loop i) = f (refl base i), but how does one "lift" that to <i> f (loop i) = <i> f (refl base i)?

$\endgroup$
1
$\begingroup$

Originally I was going to give an assurance that something like your extensionality principle must hold, but I decided to puzzle out enough cubical Agda to actually demonstrate the proof.

However, I should say that your all : ∀ i → f (loop i) = f (refl base i) is actually a digression. This is equivalent to a square with arbitrary sides, which looks like this:

$$ \require{AMScd} \begin{CD} x @>all(0)>> x \\ @VpVV \Rightarrow @VVreflV \\ x @>>all(1)> x \end{CD} $$

but something with type p ≡ refl is actually more uniform than that, because if e has that type, then e i : x ≡ x regardless of i, which is more uniform than the above square (where e i : all i0 i ≡ all i1 i), and is equivalent to a square of the form:

$$ \begin{CD} x @>refl>> x \\ @VpVV \Rightarrow @VVreflV \\ x @>>refl> x \end{CD} $$

But, if we have loop ≡ refl, we already have this sort of square, and applying f point-wise produces a new square of this type. So, the following code is accepted:

module Path
    (S1 Z : Set)
    (base : S1)
    (loop : base ≡ base)
    (f : S1 → Z)
    (x : Z)

    (sq : loop ≡ refl)
  where
  rfl : base ≡ base
  rfl = refl

  z : Z
  z = f base

  p : z ≡ z
  p i = f (loop i)

  zrfl : z ≡ z
  zrfl = refl

  hsq : p ≡ zrfl
  hsq j i = f (sq j i)

So, the bit in the HoTT book is just a consequence of the composition of 'functions'.

The more arbitrary square can be expressed using the PathP type, which is also written _[_≡_] in cubical Agda, and the proof of equivalence to the ∀ type is:

module Square
    (A : Set)
    (x y : A)
    (e₁ e₂ : x ≡ y)
    (lines : ∀ i → e₁ i ≡ e₂ i)
  where
  f₀ : x ≡ x
  f₀ = lines i0

  f₁ : y ≡ y
  f₁ = lines i1

  square : (λ i → e₁ i ≡ e₂ i) [ f₀ ≡ f₁ ]
  square i j = lines i j

If you want to fool around with cubical Agda yourself to try this out interactively, I've been using a recent Agda from the development branch with {-# OPTIONS --cubical #-}, along with this library.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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