How are cubical subtypes supposed to be used? about cubical HOT 17 CLOSED

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        (i : I) → A
hfill {φ = φ} u u0 i = hcomp (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                                      ; (i = i0) → ouc u0 })
                             (ouc u0)

Let me add this function to my list of things that need elaboration. The documentation for this is too sparse.

from cubical.

@mrakgr have you seen the documentation at https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.html?highlight=Cubical ?

from cubical.

Well yes, that is where I am copying these definitions from. I've been studying the documentation rather than the paper for the last two days. The amount of information given makes it seems like cubical subtypes are a language feature seen 100 times before such as arrays or tuples and that their purpose is completely transparent to the one first time seeing them. What do you need these subtypes for?

Now that I look at inc and ouc more closely I realize that they are the constructor and the eliminator for the cubical subtypes. So I guess they would have to be builtins. Yesterday I was peeking at the cubical issues and it seems they got renamed to something else.

As an example how confusing this is consider hfill. It has 3 different interval type in use for some reason. The pattern matching on φ = i1 and i = i0 is unintuitive. What is u (i ∧ j) 1=1 supposed to be? Why ouc u0? The cubical subtype is not even apparently used. It only came in in order to be eliminated. Apparently the documentation thinks that I can get a complete accurate model of hfill just from the x = y -> y = z -> x = z example. Surely better could be done in terms of explanation.

from cubical.

I am not sure what i ∧ j in (φ = i1) → u (i ∧ j) 1=1 is supposed to be doing, but 1=1 should be referring to φ being i1 right?

from cubical.

{-# BUILTIN SUB Sub #-}

postulate
  inc : ∀ {ℓ} {A : Set ℓ} {φ} (x : A) → Sub A φ (λ _ → x)

{-# BUILTIN SUBIN inc #-}

primitive
  primSubOut : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → Sub _ φ u → A

I admit I haven't looked the the appendix of the documentation until now. For some reason I was under the impression that the primitives were defined in the Cubical library's Core. Also, note that ouc is named primSubOut here.

...Now that I look at it more closely it I see that the module they are defined is Agda.Primitive.Core which comes with Agda itself rather than the Cubical library. My bad.

ouc and inc are named inS and outS in the Cubical library though.

from cubical.

-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ
-- Partial i A = IsOne i → A

So Partial is literally IsOne i → A? From the documentation all I got is that it is a special pattern matching feature. How do you pattern match on a function directly?

Also what about PartialP?

from cubical.

How do you pattern match on a function directly?

Ah, I see.

partialBool : ∀ i → Partial (i ∨ ~ i) Bool
partialBool i (i = i0) = true
partialBool i (i = i1) = false

This example makes sense if you think of it as ...

partialBool : ∀ i → IsOne (i ∨ ~ i) → Bool
partialBool i (i = i0) = true
partialBool i (i = i1) = false

So pattern matching on IsOne is the intended functionality of Partial. That having said if you actually try to destructure the above directly the type error is pretty nasty. The raw AST seems to be getting printed as output.

from cubical.

We have that both outS (inS v) = v and inS (outS v) = v hold if well typed. Moreover, outS v will reduce to u 1=1 when r = i1.

The Cubical Agda paper has some differences compared to the documentation. It is not obvious to me that this would hold just from the type signatures of inS and outS.

from cubical.

inS : {r : I} (a : A) → A [ r ↦ (λ _ → a) ]
outS : {r : I} {u : Partial r A} → A [ r ↦ u ] → A
outS (inS v) = v 
inS (outS v) = v

Putting things together what inS does is map variable v from type A to A [ r ↦ (λ _ → v)]. Meaning v : A maps to v : A [ r ↦ (λ _ → v)] now. I've left the names the same to highlight that the object is the same and only the type differs. What I wrote does not strictly make sense, but you can imagine variables being tagged at compile time and u and v (for example) being equal if they have the same tag.

With that in mind, it makes sense that outS could just strip out that type information from the type level and get back the same variable. Both inS and outS are just identity functions under the hood.

What I do not understand yet is why it cannot just be A [v]. Why must there be a requirement that r = i1?

from cubical.

Any term u : A can be seen as a term of type A [ r ↦ u ] that agrees with itself when IsOne r.

This is from the paper, but the documentation has the same error. Note that u cannot be A here, it needs to be a Partial.

from cubical.

(Online docs)

A term v : A [ φ ↦ u ] should be thought of as a term of type A which is definitionally equal to u : A when IsOne φ is satisfied.

(Paper)

Cubical Agda also has cubical subtypes as in Cohen et al. [2018]; given A : Set ℓ, r : I and
u : Partial r A we can form the type A [ r ↦ u ]. A term v of this type is a term of type A that is
definitionally equal to u when IsOne r is satisfied.

If what I've written two posts ago is right then this makes no sense. Which sort of explains why I've needed so much time to understand this. u and v cannot be the same type here.

from cubical.

To be precise both should say "... definitionally equal to u 1=1"

from cubical.

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        (i : I) → A
hfill {φ = φ} u u0 i =
  hcomp
    {φ = φ ∨ ~ i }
    (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
             ; (i = i0) → outS u0 })
    (outS u0)

Now that I understand to ignore outS and inS, this makes room in my mind for me to consider this again. The above is the same as hfill from the docs except with the implicit argument filled in explicitly. I wasn't sure whether it would be (i ∧ φ) ∨ ~ i or φ ∨ ~ i . The reason is the following fragment from the paper.

When i is i0 this is outS u₀ and when i is i1 it is hcomp (λ j → λ { (r = i1) → u j 1=1 } u₀ as the absurd faces (i0 = i1) gets [snip] filtered out.

In contrast to the above, the documentation is again more nonsense...

When i is i0 this is u0 and when i is i1 this is hcomp u u0.

No way does hcomp u u0 make sense.

In the code I've posted the (i = i0) → outS u0 case makes sense to me as it is just returning the original element. This matches with i = i0 case in path types.

On the other hand (φ = i1) → u (i ∧ j) 1=1 has a lot of mysteries. First of all, unlike what the paper says it does not seem like when φ = i1 that i = i1 as well.

as the absurd faces (i0 = i1) gets filtered out

I am confused as to what this part means. I thought that given the context it should mean the i = i0 /\ φ = i1, but why wouldn't that be a valid case?

When i = i0 /\ φ = i1 would it not make more sense to say that both branches just reduce to the same value meaning that u i0 1=1 = outS u0. Still, even as I write this I can't see why u i0 1=1 would reduce to this based on the definitions.

from cubical.

One more thing...

hfill' : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        (i : I) → A
hfill' {φ = φ} u u0 i =
  hcomp
    {φ = φ ∨ ~ i }
    (λ j → λ { (φ = i1) → u i0 1=1
             ; (i = i0) → outS u0 })
    (outS u0)

I find it strange that u i0 1=1 also passes typechecking here. Is that intentional?

I really wish the type system and the type errors errors were more informative of what exactly is expected of me here. I can't tell what is going on in this function at all based on the type signatures.

from cubical.

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        (i : I) → A
hfill {φ = φ} u u0 i =
  hcomp
    {φ = φ ∨ ~ i }
    (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
             ; (i = i0) → outS u0 })
    (outS u0)

Now that I understand to ignore outS and inS, this makes room in my mind for me to consider this again. The above is the same as hfill from the docs except with the implicit argument filled in explicitly. I wasn't sure whether it would be (i ∧ φ) ∨ ~ i or φ ∨ ~ i . The reason is the following fragment from the paper.

When i is i0 this is outS u₀ and when i is i1 it is hcomp (λ j → λ { (r = i1) → u j 1=1 } u₀ as the absurd faces (i0 = i1) gets [snip] filtered out.

In contrast to the above, the documentation is again more nonsense...

When i is i0 this is u0 and when i is i1 this is hcomp u u0.

No way does hcomp u u0 make sense.

I am going to ask you to moderate your tone when talking about other people's work.
However, you're welcome to ask questions and point out where you find the documentation confusing.

In particular hcomp u (outS u0) is indeed what hfill u u0 i1 is equal to.

In the code I've posted the (i = i0) → outS u0 case makes sense to me as it is just returning the original element. This matches with i = i0 case in path types.

On the other hand (φ = i1) → u (i ∧ j) 1=1 has a lot of mysteries. First of all, unlike what the paper says it does not seem like when φ = i1 that i = i1 as well.

The paper did not intend to say that φ = i1 implies i = i1, can you point out where it seems like it did?

as the absurd faces (i0 = i1) gets filtered out

I am confused as to what this part means. I thought that given the context it should mean the i = i0 /\ φ = i1, but why wouldn't that be a valid case?

That part of the sence is still talking about the i = i1 case. If you substitute i1 for i in the body of hfill you get

  hcomp
    {φ = φ ∨ ~ i1 }
    (λ j → λ { (φ = i1) → u i0 1=1
             ; (i1 = i0) → outS u0 })
    (outS u0)

and the (i1 = i0) → outS u0 branch will then be discarded/ignored because we can never have i1 = i0.

When i = i0 /\ φ = i1 would it not make more sense to say that both branches just reduce to the same value meaning that u i0 1=1 = outS u0. Still, even as I write this I can't see why u i0 1=1 would reduce to this based on the definitions.

Indeed if i = i0 /\ φ = i1 holds then u i0 1=1 = outS u0, that is guaranteed by the type of u0 and by how outS computes, and u i0 1=1 is also the value the whole hcomp ... will reduce to in this case. However, to clarify, this wasn't the case the quoted sentence was talking about.

Regarding your hfill', yes that code is also fine, however it doesn't serve the same purpose.

A more precise type for hfill would be (with hcomp typed as in the library):

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        → PathP (\ _ → A) (outS u0) (hcomp u (outS u0))

stating that an hcomp is connected to its base u0.

from cubical.

  hcomp
    {φ = φ ∨ ~ i1 }
    (λ j → λ { (φ = i1) → u i0 1=1
             ; (i1 = i0) → outS u0 })
    (outS u0)

Did you make a mistake in substituting i for i0 in the first branch (φ = i1) → u i0 1=1? I'd expect this to be (φ = i1) → u j 1=1 once i1 ∧ j gets reduced. I am guessing you probably pasted and modified the erroneous example in my last post. I'll go with that assumption for now.

In particular hcomp u (outS u0) is indeed what hfill u u0 i1 is equal to.

hfill {φ = φ} u u0 i =
  hcomp
    {φ = φ ∨ ~ i }
    (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
             ; (i = i0) → outS u0 })
    (outS u0)

How could that be the case? Even if you know that i = i1, the most you can reduce hfill should be...

  hcomp
    {φ = φ }
    (λ j → λ { (φ = i1) → u j 1=1
             ; (i1 = i0) → outS u0 })
    (outS u0)

This is a far cry from reducing it to hcomp u (outS u0). Even ignoring the implicit argument, I do not see a way of how you could reduce lambda to just u.

Indeed if i = i0 /\ φ = i1 holds then u i0 1=1 = outS u0, that is guaranteed by the type of u0 and by how outS computes, and u i0 1=1 is also the value the whole hcomp ... will reduce to in this case. However, to clarify, this wasn't the case the quoted sentence was talking about.

I think I made a mistake with the order I took in my post. I got sucked into the pace of the paper and said that...

When i is i0 this is outS u₀ and when i is i1 it is hcomp (λ j → λ { (r = i1) → u j 1=1 } u₀

But really, instead of saying that when i is 'when i is i0 this is outS u₀', what I really need to do is consider the i = i0 /\ φ = i0 and i = i0 /\ φ = i1 cases separately.

i = i0 /\ φ = i0

This just reduces to outS u0. And since φ = i0 the outS just strips the [ φ ↦ u i0 ] part from u0's type without any additional work being done.

i = i0 /\ φ = i1

Here both branches are valid and reduce to u i0 1=1 and outS u0 respectively and it is necessary to prove that both of them are definitionaly equal. In the later branch what is now known is that u0 is of type A [ i1 ↦ u i0 ]. So then outS can use that as proof that u0 is definitionally equal to u i0 1=1.

Let me also consider the other two possibilities.

i = i1 /\ φ = i0

This one is absurd so there is no need to consider it.

i = i1 /\ φ = i1

This one reduces to u j 1=1.

Actually I still have some questions about this. If I were to interpret as what this is doing, it does seem like u : ∀ i → Partial i1 A is acting exactly like a path type here.

...Though in path types, if you have something like x ≡ y, you can always refer to x and y explicitly. Here that seems to have vanished and only the type of the elements is known.

This is a bit confusing as expected. Why isn't there something like a PartialPath φ x y in order to have this kind of mechanism resemble regular propositional equality more?

Now that I think about it, I am sure you would need path types to implement a nontrivial function of ∀ i → Partial φ A.

from cubical.

hfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
        (u : ∀ i → Partial φ A) (u0 : A [ φ ↦ u i0 ])
        → outS u0 ≡ hcomp u (outS u0)
hfill {φ = φ} u u0 i =
  hcomp
    {φ = φ ∨ ~ i }
    (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
             ; (i = i0) → outS u0 })
    (outS u0)

In particular hcomp u (outS u0) is indeed what hfill u u0 i1 is equal to.

Since this typechecks I guess you weren't lying when you said this.

Now that I look at it more closely, u is in fact the same as λ j → λ { (φ = i1) → u j 1=1 }. I keep thinking that hcomp expects an element of A when it actually expects λ { (φ = i1) → u j 1=1 } which is a Partial. Also applying 1=1 to u j isn't quite the same as eta reduction so I did not realize this.

With this I have a complete mental model of how hfill and homogeneous compositions work. Thank you very much for helping fill in the blanks. I'll close this here, but feel free if you want to add any more comments.

from cubical.