Cubical discussion forum about cubical HOT 89 CLOSED

Is there a specific reason why compIso is implemented as:

compIso : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''} →
Iso A B → Iso B C → Iso A C
compIso i j = equivToIso (compEquiv (isoToEquiv i) (isoToEquiv j))

instead of for example

compIso₂ : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''} →
Iso A B → Iso B C → Iso A C
compIso₂ (iso fun inv rightInv leftInv) (iso fun₁ inv₁ rightInv₁ leftInv₁) = iso (fun₁ ∘ fun) (inv ∘ inv₁)
(λ b → cong fun₁ (rightInv (inv₁ b)) ∙ (rightInv₁ b))
(λ a → cong inv (leftInv₁ (fun a) ) ∙ leftInv a )

?

I encountered errors in Agda (not fatal error but typechecking goes infinitely) with the first definition,
but everything works with the second.

from cubical.

@oisdk I'm writing a tutorial for Cubical Agda using literate agda:

• https://ice1000.org/2019/08/01/Cutt0/
• https://ice1000.org/2019/08/20/Cutt1/
• https://ice1000.org/2019/10/01/Cutt2/
• https://ice1000.org/2019/10/14/Cutt3/

from cubical.

I'm not sure what this is or what it achieves... Can you elaborate a bit on why it might be useful?

@mortberg Checkout the Agda documentation: https://agda.readthedocs.io/en/latest/language/with-abstraction.html#the-inspect-idiom

from cubical.

This might be a good idea. Maybe we should call it Type instead of U though?

I like Type!

from cubical.

This is what I went with in the end:

path u a v b {p} {q} x i plus path u₁ a₁ v₁ b₁ {p₁} {q₁} x₁ j =
  isSet→isSet' trunc
    (plus-lemma1 u a u₁ a₁ v₁ b₁ p p₁ q₁ x₁)
    (plus-lemma1 v b u₁ a₁ v₁ b₁ q p₁ q₁ x₁)
    (plus-lemma2 u₁ a₁ u a v b p₁ p q x)
    (plus-lemma2 v₁ b₁ u a v b q₁ p q x)
    i j

from cubical.

@oisdk Here is a probably incomplete list we are keeping on the HoTT wiki.

Edit: Sorry this is about cubical type theory. The only paper specifically about cubical agda is this one. Since it is still early days, I doubt many others have written about it yet.

from cubical.

Here's a proof. You don't need to know that A and B are sets.

{-# OPTIONS --cubical --safe #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence

pathExtensionality : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
  → (∀ (a : A) → transport p a ≡ transport q a) → p ≡ q
pathExtensionality {p = p} {q} w i =
  hcomp
    (λ j → λ
      { (i = i0) → secEq univalence p j
      ; (i = i1) → secEq univalence q j
      })
    (invEq univalence ((λ a → w a i) , t i))
  where
  t : PathP (λ i → isEquiv (λ a → w a i)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→isContrPathP isPropIsEquiv (λ i a → w a i) _ _ .fst

If p and q come from isoToPath then there should be a more direct proof, but it seems to be something of a pain to write because isoToPath is not the same as ua ∘ isoToEquiv (or so Agda tells me, although I can't see the difference looking at the definitions...)

from cubical.

Btw, who are you @3abc ? Your github profile is very mysterious.

from cubical.

Btw, who are you @3abc ? Your github profile is very mysterious.

Sent you an email (to your CMU mailbox).

from cubical.

Anyone know how to generalize this proof?

mapHLevel : ∀ {ℓ} {A B : Set ℓ} (n : ℕ) (p : isOfHLevel n B) → isOfHLevel n (A → B)
mapHLevel 0 p = (λ _ → p .fst) , λ y i a → snd p (y a) i
mapHLevel 1 p a b i x = p (a x) (b x) i
mapHLevel 2 p a b x y i j z = p (a z) (b z) (λ i → x i z) (λ i → y i z) i j 
mapHLevel 3 p a b x y r s i j k z = p (a z) (b z) (λ i → x i z) (λ i → y i z) (λ i j → r i j z) (λ i j → s i j z) i j k 
mapHLevel (suc (suc n)) p a b = {!!}

The pattern is clear but I don't know how to implement the induction step.

from cubical.

@3abc In the redtt library, we have a general version of this: https://github.com/RedPRL/redtt/blob/master/library/paths/pi.red#L17

from cubical.

@3abc In the redtt library, we have a general version of this: https://github.com/RedPRL/redtt/blob/master/library/paths/pi.red#L17

Oh thank you. That's great.

from cubical.

@3abc In the redtt library, we have a general version of this: https://github.com/RedPRL/redtt/blob/master/library/paths/pi.red#L17

Does redtt's highlighting mean something? For the name pi/hlevel I see pi in black and /hlevel in red. Is this just a general name or something special?

from cubical.

Does redtt's highlighting mean something? For the name pi/hlevel I see pi in black and /hlevel in red. Is this just a general name or something special?

I think that whatever GitHub is doing for highlighting is essentially random 🤣

from cubical.

I think that whatever GitHub is doing for highlighting is essentially random 🤣

I believe GitHub is highlighting it as if it were Red because ofthe .red file extension.

from cubical.

@3abc mapHLevel is an instance of Cubical.Foundations.HLevels.hLevelPi iiuc

from cubical.

@3abc mapHLevel is an instance of Cubical.Foundations.HLevels.hLevelPi iiuc

Ah so this exists. One of the current PR can use that.

from cubical.

I have a question about Cubcial Agda. I'm trying to prove plus commutes on HitInt.
Imports:

open import Cubical.Core.Everything
open import Cubical.Data.Nat
  renaming ( +-comm to :+:-comm
           ; +-zero to :+:-zero
           ; _+_ to _:+:_
           )
open import Cubical.HITs.HitInt renaming (_+ℤ_ to _+_; ℤ to Z)

I have these lemmas:

+-zero : ∀ a → pos 0 + a ≡ a
+-zero (pos zero) = refl
+-zero (pos (suc n)) = cong sucℤ (+-zero (pos n))
+-zero (neg zero) = posneg
+-zero (neg (suc n)) = cong predℤ (+-zero (neg n))
+-zero (posneg i) j = posneg (i ∧ j)

+-i-zero : ∀ a i → posneg i + a ≡ a
+-i-zero a i = cong (_+ a) (λ j → posneg (i ∧ ~ j)) ∙ +-zero a
+-pos-suc : ∀ a b → sucℤ (pos b + a) ≡ (pos (suc b) + a)
+-pos-suc (pos zero) b = refl
+-pos-suc (pos (suc n)) b = cong sucℤ (+-pos-suc (pos n) b)
+-pos-suc (neg zero) b = refl
+-pos-suc (neg (suc n)) b =
  sucPredℤ (pos b + neg n)
  ∙ sym (predSucℤ (pos b + neg n))
  ∙ cong predℤ (+-pos-suc (neg n) b)
+-pos-suc (posneg i) b = refl

+-neg-pred : ∀ a b → predℤ (neg b + a) ≡ (neg (suc b) + a)
+-neg-pred (pos zero) b = refl
+-neg-pred (pos (suc n)) b =
  predSucℤ (neg b + pos n)
  ∙ sym (sucPredℤ (neg b + pos n))
  ∙ cong sucℤ (+-neg-pred (pos n) b)
+-neg-pred (neg zero) b = refl
+-neg-pred (neg (suc n)) b = cong predℤ (+-neg-pred (neg n) b)
+-neg-pred (posneg i) b = refl

All the code above checks. My proof is almost finished, but one part is left:

+-comm : (a b : Z) → a + b ≡ b + a
+-comm a (pos zero) = sym (+-zero a)
+-comm a (neg zero) = sym (cong (_+ a) (sym posneg) ∙ +-zero a)
+-comm a (pos (suc b)) = cong sucℤ (+-comm a (pos b)) ∙ +-pos-suc a b
+-comm a (neg (suc b)) = cong predℤ (+-comm a (neg b)) ∙ +-neg-pred a b

I didn't finish the last clause:

+-comm a (posneg i) = {sym (+-i-zero a i) }0

Agda tells me that the goal's type is a = posneg i + a while my code sym (+-i-zero a i) has exactly the same time. However, when I try to fill the hole, it says:

+-zero a (~ i) !=
hcomp
(λ { j ((~ (~ i) ∨ ~ i) = i1)
       → (λ { ((~ i) = i0) → posneg (i0 ∧ ~ i0) + a
            ; ((~ i) = i1) → +-zero a (i1 ∧ j)
            })
         _
   ; j (i1 = i0) → ouc (inc (posneg (i0 ∧ ~ (~ i)) + a))
   })
(ouc (inc (posneg (i0 ∧ ~ (~ i)) + a)))
of type Z
when checking the definition of +-comm

I can't read this error, it's too complicated to me. Can anyone explain this to me?
I understand how demorgan interval operations work, but I'm not familiar with things like hcomp and the implementation of Cubical Agda.

from cubical.

Can anyone explain this to me?

Is this file committed to your fork so we can see it in some branch?

from cubical.

No, it's not in a fork but in my personal study code repo: https://github.com/ice1000/learn/blob/master/Agda/SymInt.agda

from cubical.

The code file is commited with the goal removed but it doesnt check.

from cubical.

I can't read this error, it's too complicated to me.

Oh I think you got mislead by the type given by Agda. Read this #68 (comment). It's currently misleading when HITs are involved. The type Agda gave you is actually wrong in some sense. You have to figure out the real type.

from cubical.

Basically you want a term L isuch that not only it proves a ≡ (posneg i + a), but at the endpoints i = i0 and i = i1 it proves a ≡ (posneg i + a) in a particular way.

For example when i = i0, L i0 should be equal to +-comm a (pos 0) you defined above (because posneg i0 is the same as pos 0). In this case your attempted term isn't.

from cubical.

What you need in the last line is a more complicated term:

+-comm a (posneg i) = L i
  where
  L : PathP (λ i → (a + posneg i) ≡ (posneg i + a)) (sym (+-zero a)) (sym (cong (_+ a) (sym posneg) ∙ +-zero a))
  L = { }0

The two end points are exactly your definition of +-comm a (pos 0) and +-comm a (neg 0), which is what I meant by "a particular way".

from cubical.

I'm sorry but maybe I'm noober than you may expect me to be. In your linked comment,

However this attempt will fail because the value of ?1 when x = i0 or x = i1 needs to be the same as f base.

Could you elaborate? Why do they need to be equal to f base? I didn't see any indication of this.

from cubical.

Could you elaborate? Why do they need to be equal to f base? I didn't see any indication of this.

If you work in an HIT A and there's a higher constructor p : Path A a b, to get a term f : A → B you cannot just define f (p i) to be anything in B, the path λ i → (f (p i)) has to be of type Path B (f a) (f b). Make sense?

from cubical.

Yes, I agree.

I feel like I get the idea for some sense, the equality structure should be preserved when pattern matching on a higher constructor. In my case, I need to preserve the structure for my previous equality proofs, right?

from cubical.

Yes, I agree.

I feel like I get the idea for some sense, the equality structure should be preserved when pattern matching on a higher constructor. In my case, I need to preserve the structure for my previous equality proofs, right?

Yeah, when you want to define a function f, its action on a higher constructor have to behave like a cong. (For higher paths, "higher" cong.)

from cubical.

The type Agda gave you is actually wrong in some sense.

@3abc @ice1000 The type is not wrong, it's however not the whole story. I'm sorry if I keep going over this point but it's becoming frustrating for things to be misrepresented in this way.

See agda/agda#3606 (comment) for another example where the type of the goal is also not communicating all the constraints to satisfy, while having nothing to do with HITs.

If you load SymInt.agda you will also see constraints for the goal ?1, one of them is fairly large, because that's what the particular call of _∙_ reduces to.

from cubical.

The type Agda gave you is actually wrong in some sense.

@3abc @ice1000 The type is not wrong, it's however not the whole story. I'm sorry if I keep going over this point but it's becoming frustrating for things to be misrepresented in this way.

OK! Thanks for the clarification.

from cubical.

Is there a way to inline f in this proof of singleton being a set?

data T : Set where
  a : T

TSet : isSet T
TSet a a p q i j =
  hcomp (λ k → λ { (i = i0) → f (p j) k
                 ; (i = i1) → f (q j) k
                 ; (j = i0) → a
                 ; (j = i1) → a
                 }) a
  where
  f : (y : T) → a ≡ y
  f a i = a

from cubical.

@3abc the fact that agda calls its universes Set makes this awfully confusing to read, I wonder if we can rename it?

from cubical.

@3abc the fact that agda calls its universes Set makes this awfully confusing to read, I wonder if we can rename it?

We could. Maybe rename Set as U in prelude? @mortberg what do you think?

from cubical.

Then u lose universal polymorphism. I recommend

U : (l : Level) -> Set (lsuc l)
U l = Set l

U0 = U lzero

from cubical.

Is there something like inspect in the cubical lib? It may be necessary when using paths as the equality type to prove something.

record Reveal_·_is_ {a b} {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (ℓ-max a b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

from cubical.

Then u lose universal polymorphism. I recommend

U : (l : Level) -> Set (lsuc l)
U l = Set l

U0 = U lzero

This might be a good idea. Maybe we should call it Type instead of U though?

from cubical.

Is there something like inspect in the cubical lib? It may be necessary when using paths as the equality type to prove something.

record Reveal_·_is_ {a b} {A : Set a} {B : A → Set b}
                    (f : (x : A) → B x) (x : A) (y : B x) :
                    Set (ℓ-max a b) where
  constructor [_]
  field eq : f x ≡ y

inspect : ∀ {a b} {A : Set a} {B : A → Set b}
          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
inspect f x = [ refl ]

I'm not sure what this is or what it achieves... Can you elaborate a bit on why it might be useful?

from cubical.

@mortberg I think the role of the "inspect idiom" in Agda is to be able to pattern match on a compound expression using a with statement (like with f (g x)), but still remember that each of the clauses is related to f (g x) somehow.

It is basically giving a dependent induction principle to the sigma type (y : Z) * y = (f (g x)).

from cubical.

A very basic question:

We did

open import Agda.Primitive.Cubical public
  renaming ( primIMin       to _∧_  -- I → I → I
           ; primIMax       to _∨_  -- I → I → I
           ; primINeg       to ~_   -- I → I
           )

in Primitives.agda, but I don't see anything mentioned about their fixities.

What are the default fixity and associativity of these operators?

from cubical.

Hi,

So, I'm working on defining a HIT for modular numbers. The idea is that you have paths between n and k+n in Modulo k. I wanted to define a mapping to more ordinary finite sets, and I thought it might be a good opportunity to do something similar to the homotopy patch theory stuff, where you turn the paths in the HIT into paths between singleton types. However, I hit a wall where I don't know what to write, and I'm not sure there are any other examples. Here's the spot:

https://github.com/dolio/cubical/blob/master/Cubical/HITs/Modulo/Base.agda#L123

Is my assumption that I need glue correct? I tried transporting reduce _ n along i ∧ j but it unfortunately it didn't work. Maybe I should actually go back and look at the patch theory paper.

Edit: Actually, I think I know what I have to do. I need to define a path between reduce k n and reduce k (suc k + n), which will involve the transport I'm doing being a path.

from cubical.

@3abc if you check Agda.Primitive.Cubical you can see the infix declarations. Renaming keeps the same fixities.

infix  30 primINeg
infixr 20 primIMin primIMax

from cubical.

Edit: Actually, I think I know what I have to do. I need to define a path between reduce k n and reduce k (suc k + n), which will involve the transport I'm doing being a path.

@dolio I find making equalities homogeneous is easier to use. So your squash constructor can be defined with the homogeneous path Path (or just \equiv) instead of heterogeneous path PathP.

from cubical.

can one write a HIT where the constructors cannot be sorted by dimensions?

If I understand correctly, the constructors of a HIT can reference the previously defined constructor, and each one can have arbitrary dimension, so it is possible to write for example this:

nothing : {t : Set} → (a : t) → Set
nothing a = ℕ

data U : Set where
  a : U
  b : (t : U) → t ≡ t
  c : (d : nothing b) → U

where b has higher dimension, but is defined before c, and c references b.

But the previous example is "trivial" because c's dependency on b is non-essential.

1. can we write one that have essentially out-of-order dependency?
2. is there a natural example in math/cs?

from cubical.

So, here's something I've been bumping into from time to time. The best example I can think of is propositional truncation.

To use the eliminator, you need to specify a family ∥ A ∥ → Set ℓ. If you want to get fancy an define it by case analysis, the higher constructor requires exhibiting a type path that behaves correctly at the end points. For some types this is fine, because the endpoints are other constructors, so the types of the endpoints reduce. But the truncation constructor's endpoints are arbitrary other values from the constructor, so the endpoints are abstract. You could do case analysis on those values, but that just results in more copies of the problem.

Is there any way to give such a family by cases? Or can it only be defined uniformly?

from cubical.

@dolio This paper does say that functions ∥ A ∥ → Set ℓ are equivalent to maps A → Set ℓ plus an infinite tower of coherence conditions.

In specific cases you should be able to do better, but I would expect you need something like a mutual induction at least.

from cubical.

Ah, I see. I guess that paper suggests a method. The tower gets truncated to the dimension of the target. So it is unlikely that you would not expect to define ∥ A ∥ → Set ℓ by cases, but perhaps ∥ A ∥ → hSet ℓ is feasible for instance (assuming I'm correct about that having finite dimension).

from cubical.

Yep, hSet is a groupoid, so it's finitely truncated.

from cubical.

Is there a specific reason why compIso is implemented as:

compIso : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''} →
Iso A B → Iso B C → Iso A C
compIso i j = equivToIso (compEquiv (isoToEquiv i) (isoToEquiv j))

instead of for example

compIso₂ : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ} {B : Set ℓ'} {C : Set ℓ''} →
Iso A B → Iso B C → Iso A C
compIso₂ (iso fun inv rightInv leftInv) (iso fun₁ inv₁ rightInv₁ leftInv₁) = iso (fun₁ ∘ fun) (inv ∘ inv₁)
(λ b → cong fun₁ (rightInv (inv₁ b)) ∙ (rightInv₁ b))
(λ a → cong inv (leftInv₁ (fun a) ) ∙ leftInv a )

?

I encountered errors in Agda (not fatal error but typechecking goes infinitely) with the first definition,
but everything works with the second.

Haha, no, there is no deep reason for the current proof. It is obviously very inefficient so please make a PR with your better proof.

from cubical.

I'm currently trying to implement addition on rational numbers. I have already implemented lots of necessary properties of integers (e.g. associativity, commutativity, distributivity on addition and multiplication), and they have allowed me to write implementations of most of the cases for rational addition (specifically con plus con, con plus path, path plus con, trunc plus anything, anything plus trunc), but I am stuck on the case of path plus path. I think a solution would involve hcomp, but I have been struggling to find something that satisfies the constraint checker. I still do not really understand hcomp, hfill and co. Some more documentation around these tools might be handy.

Some specifics:

I am using instance arguments to overload common operators, so no need for +ℤ, +ℚ etc. I also have FROMNAT and FROMNEG defined for natural numbers, integers and rationals.

I have the following helpers defined:

nonzero-prod : (q r : ℤ) → ¬ (q ≡ 0) → ¬ (r ≡ 0) → ¬ (q * r ≡ 0)

plus_lemma1 : (u a v b w c : ℤ)
  (x : ¬ a ≡ 0) (p₁ : ¬ b ≡ 0) (p₂ : ¬ c ≡ 0)
  (y : v * c ≡ w * b)
  → con (u * b + v * a) (a * b) (nonzero-prod a b x p₁) ≡ con (u * c + w * a) (a * c) (nonzero-prod a c x p₂)

plus_lemma2 : (u a v b w c : ℤ)
  (x : ¬ a ≡ 0) (p₁ : ¬ b ≡ 0) (p₂ : ¬ c ≡ 0)
  (y : v * c ≡ w * b)
  → con (v * a + u * b) (b * a) (nonzero-prod b a p₁ x) ≡ con (w * a + u * c) (c * a) (nonzero-prod c a p₂ x)

The definition of addition on ℚ looks like this:

instance
  ℚ+ : Op+ ℚ ℚ (const₂ ℚ)
  _+_ ⦃ ℚ+ ⦄ q r = q plus r where
    _plus_ : ℚ → ℚ → ℚ
    con u a x plus con v b y = con (u * b + v * a) (a * b) (nonzero-prod a b x y)
    con u a x plus path v b w c {p₁} {p₂} y i = plus_lemma1 u a v b w c x p₁ p₂ y i
    path v b w c {p₁} {p₂} y i plus con u a x = plus_lemma2 u a v b w c x p₁ p₂ y i
    path u a v b {p} {q} x i plus path u₁ a₁ v₁ b₁ {p₁} {q₁} x₁ j = ?
    q@(path _ _ _ _ _ _) plus trunc r r₁ x y i i₁ = trunc (q plus r) (q plus r₁) (cong (q plus_) x) (cong (q plus_) y) i i₁
    q@(con _ _ _) plus trunc r r₁ x y i i₁ = trunc (q plus r) (q plus r₁) (cong (q plus_) x) (cong (q plus_) y) i i₁
    trunc q q₁ x y i i₁ plus r = trunc (q plus r) (q₁ plus r) (cong (_plus r) x) (cong (_plus r) y) i i₁

(The duplicate cases with @ above are to satisfy --exact-split).

The part I am having trouble with is the hole in the path plus path case.

I have made the following attempts to fill it:

1. (I can't find a way to fill in both the (j = i1) case and the (i = i1) case at the same time)

hcomp (λ k → \ { (i = i0) → plus_lemma1 u a u₁ a₁ v₁ b₁ p p₁ q₁ x₁ (j ∧ k)
               ; (i = i1) → compPath-filler (plus_lemma2 u₁ a₁ u a v b p₁ p q x) (plus_lemma1 v b u₁ a₁ v₁ b₁ q p₁ q₁ x₁) j k
               ; (j = i0) → plus_lemma2 u₁ a₁ u a v b p₁ p q x (i ∧ k)
               ; (j = i1) → ? -- can't find anything that will fit here
               })
      (con (u * a₁ + u₁ * a) (a * a₁) (nonzero-prod a a₁ p p₁))

2. (filling in the (j = i1) case causes the constraint checker to be unhappy)

hcomp (λ k → \ { (i = i0) → plus_lemma1 u a u₁ a₁ v₁ b₁ p p₁ q₁ x₁ (j ∧ k)
               ; (i = i1) → plus_lemma1 v b u₁ a₁ v₁ b₁ q p₁ q₁ x₁ (j ∧ k)
               ; (j = i0) → plus_lemma2 u₁ a₁ u a v b p₁ p q x i
               ; (j = i1) → doubleCompPath-filler ? (plus_lemma2 v₁ b₁ u a v b q₁ p q x) ? i (~ k)
               })
      (plus_lemma2 u₁ a₁ u a v b p₁ p q x i)

3. (this just doesn't work at all, but I thought it might be close to a solution)

doubleCompPath-filler
  (sym $ plus_lemma1 u a u₁ a₁ v₁ b₁ p p₁ q₁ x₁)
  (plus_lemma2 u₁ a₁ u a v b p₁ p q x)
  (plus_lemma1 v b u₁ a₁ v₁ b₁ q p₁ q₁ x₁)
  i j

How do I go about building an intuition for proofs like this? I currently feel like I'm stabbing in the dark.

from cubical.

@dylanede Could you make a branch on your own fork so we can see what you have done?

from cubical.

@Alizter, sure, I've just tidied it up. It is all just an experiment in a single file at the moment as I get to grips with everything. I haven't tried to reorganise it as a branch of this repository yet.

https://github.com/dylanede/cubical-experiments

from cubical.

I think what it boils down to is defining a square, i.e.

Square : ∀ {ℓ} {A : Set ℓ} {x0 x1 y0 y1 : A} →
           x0 ≡ x1 → y0 ≡ y1 → x0 ≡ y0 → x1 ≡ y1 → Set ℓ
Square p q r s = PathP (λ i → p i ≡ q i) r s

square : ∀ {ℓ} {A : Set ℓ} {x0 x1 y0 y1 : A} →
           (p : x0 ≡ x1) → (q : y0 ≡ y1) → (r : x0 ≡ y0) → (s : x1 ≡ y1) → Square p q r s
square p q r s i j = ?

Is there a way of filling the hole in the above snippet?

from cubical.

@dylanede square is the same as isSet' A

from cubical.

@dolio, thank you that's very helpful! I'm now using isSet→isSet' in combination with trunc.

from cubical.

After updating library to its newest version 3335976
from 0249030

I get an error for deffinition of fill in Core/Primitives

fill : (A : ∀ i → Type (ℓ′ i))
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i
fill A {φ = φ} u u0 i =
  comp (λ j → A (i ∧ j))
       (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                ; (i = i0) → outS u0 })
       (outS u0)

/agdaLibs/cubical/Cubical/Core/Primitives.agda:193,3-196,16
A (i ∧ i0) → A (i ∧ i1) !=< A i of type
Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1)))
when checking that the inferred type of an application
  A (i ∧ i0) → A (i ∧ i1)
matches the expected type
  A i

I am using 2.6.0 version of agda.
What can cause such a problem?

from cubical.

After updating library to its newest version 3335976
from 0249030

I get an error for deffinition of fill in Core/Primitives

fill : (A : ∀ i → Type (ℓ′ i))
       {φ : I}
       (u : ∀ i → Partial φ (A i))
       (u0 : A i0 [ φ ↦ u i0 ])
       ---------------------------
       (i : I) → A i
fill A {φ = φ} u u0 i =
  comp (λ j → A (i ∧ j))
       (λ j → λ { (φ = i1) → u (i ∧ j) 1=1
                ; (i = i0) → outS u0 })
       (outS u0)

/agdaLibs/cubical/Cubical/Core/Primitives.agda:193,3-196,16
A (i ∧ i0) → A (i ∧ i1) !=< A i of type
Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1)))
when checking that the inferred type of an application
  A (i ∧ i0) → A (i ∧ i1)
matches the expected type
  A i

I am using 2.6.0 version of agda.
What can cause such a problem?

I merged a patch to Agda that changed the implicit arguments to comp. I then updated the library accordingly in: #142

So the library once again only compile on the development version of Agda. For detailed instructions how to install this see: https://github.com/agda/cubical/blob/master/INSTALL.md

We will hopefully not have to do many more changes like this that are not backwards compatible in the future.

from cubical.

Please let me know if this thread is not a place for such a question.

I am trying to grasp the philosophy behind some design choices in the cubical library.

It is trivial to prove, that : (Dec A) ≡ ((A ⊎ (¬ A))),
with such equality you can use lemmas about ⊎ when dealing with Dec A,
but in my experience this "translation" when introduced in lots of places tends to slower evaluation of code, and leads to obfuscated goals.

Why Dec A is not defined as (A ⊎ (¬ A)) in the cubical library?
(like in HoTT library https://github.com/HoTT/HoTT-Agda/blob/80164162ffaa4de55f87ded7b471687313aa5921/core/lib/Base.agda#L473 )

Is the main reason is the ability to pattern match on familiar "yes" and "no" rather than cryptic "inl" and "inr" ?
Or maybe problems experienced by me are expected to fade away in a future version of cubical agda?
Or maybe such trivial equality of types should be treated painlessly and I am doing something wrong?

from cubical.

Probably Dec A is like that because that's how it is in the standard library.

It has its benefits, for example with the current algorithm it's more efficient to check whether Dec A = Dec B if Dec is its own datatype rather than defined with ⊎.

It could be worth changing it anyway, especially because it's a simple type, though I wonder how much we have that's proven about ⊎. (We can use the pattern keyword to define yes and no).

Or maybe problems experienced by me are expected to fade away in a future version of cubical agda?

It should get better, we have some things planned we haven't gotten around yet, though it would be good to report the problems you face as separate issues so we have a benchmark.
That way we can also see if your code could be optimized.

In general I suggest to use copatterns to define elements of records, so you'll get smaller normal forms.

from cubical.

So, I've been fiddling around with various stuff related to the delooping of a group. I was trying to do the encode-decode trick from the HoTT book with the aim of showing that the loop space of the delooping is equivalent to the original group. However, I got into a situation where I could only figure out how to prove something via seemingly very redundant means. Here's a reconstruction of the essence:

module _ (A : Type₀) (_⊙_ : A → A → A) (eqv : ∀ a → isEquiv (_⊙ a)) where
  P : A → A ≡ A
  P x = ua (_⊙ x , eqv x)

  data Ex : Type₀ where
    base : Ex
    loop : A → base ≡ base
    surf : ∀ x y → PathP (λ i → base ≡ loop y i) (loop x) (loop (x ⊙ y))

  code : Ex → Type₀
  code base = A
  code (loop x i) = P x i

  lemma : ∀ x y z → PathP (λ i → P y i) x z
        → PathP (λ i → base ≡ loop y i) (loop x) (loop z)
  lemma x y z p i
    = hcomp (λ k → λ where
              (i = i0) → loop x
              (i = i1) → loop (hcomp (λ _ → λ where
                                (k = i0) → x ⊙ y
                                (k = i1) → z)
                                (unglue (k ∨ ~ k) (p k)))
            ) (surf x y i)
  
  decode : (e : Ex) → code e → base ≡ e
  decode base x = loop x
  decode (loop y i) gl = lemma x y z p i
    where
    x = coei→0 (λ i → P y i) i gl
    z = coei→1 (λ i → P y i) i gl
    p : PathP (λ i → P y i) x z
    p j = coei→j (λ i → P y i) i j gl

The 'issue' as it were is the loop case of decode and the lemma. This is the only way I found to prove it. The 'glue' value gl is cast to three different points just to allow surf to work out to the right type. I spent a while playing with glue and unglue stuff, which I think improved my understanding of what they do, but I still couldn't figure out a more direct formulation of this case (trying to normalize it takes a very long time, I think, as well).

Is there some better way to write this? Possibly even surf should be changed in some way, I'm not sure.

from cubical.

Here's a possibility with respect to my previous question. We can use an alternate constructor:

sheet : ∀ y → PathP (λ i → P y i → base ≡ loop y i) loop loop

And then the loop case of decode is straight forward. I'm not sure where this will lead me, but it seems like it might be promising.

from cubical.

@dolio sheet looks quite interesting, tell me if you find any bugs with that path of function type approach, it's a fairly exotic constructor.

from cubical.

So, it turns out I was really just delaying the inevitable, because having sheet as a constructor leads to you needing an equivalent construction on paths between types (for my use case). So I needed to learn how to write it from scratch anyway. Here's how you do so (note, I've swapped the arguments to surf):

sheet : ∀ g → PathP (λ i → path g i → Path (Deloop G) base (loop g i)) loop loop
sheet g i h j
  = hcomp (λ where
      k (i = i0) → surf g h (~ k) j
      k (i = i1) → loop h j
      k (j = i0) → base
      k (j = i1) → loop g (i ∨ ~ k)) (loop (unglue (i ∨ ~ i) h) j)

from cubical.

Can we turn to Gitter? @mortberg It's easy to setup a gitter chat room service for a GitHub repo. It's free.

from cubical.

@dolio It doesn't look too bad as a lemma though, is decode cleaner overall then?

from cubical.

I think it's about the same. My original reason for avoiding it was that I didn't understand how to write it that way. It took me like a week of off-and-on experiments to figure it out. But now I think I understand some stuff a little better, so hopefully that carries over to future stuff.

from cubical.

Does anyone know of a collection of papers/projects using cubical Agda?

from cubical.

I wrote a blog post on the HoTT blog about Cubical Agda last year (https://homotopytypetheory.org/2018/12/06/cubical-agda/), but that is somewhat outdated and mostly superseded by the Cubical Agda paper that we had at ICFP this year (see the link of @Alizter). There was a nice talk at the HoTT conference in August about some work on finite multisets that had been formalized in Cubical Agda: https://hott.github.io/HoTT-2019//conf-slides/Choudhury.pdf. Apart from these I can't think of any papers/talks reporting on projects using Cubical Agda. There are plenty of things one can work on though, for example: applications of Cubical Agda in CS/PL and doing more of HoTT cubically.

from cubical.

Thanks for the links! I'm doing a project using cubical Agda myself at the moment and any papers/code examples I can find are super helpful.

Would it make sense to collect these things somewhere (maybe in a wiki for this repo)?

Also there is one other project (a master's thesis) that I found which uses cubical Agda specifically: Univalent Categories.

from cubical.

but that is somewhat outdated and mostly superseded by the Cubical Agda paper that we had at ICFP this year

I've got an updated version: https://ice1000.org/lagda/CubicalAgdaLiterate.html

from cubical.

Thanks for the links! I'm doing a project using cubical Agda myself at the moment and any papers/code examples I can find are super helpful.

Would it make sense to collect these things somewhere (maybe in a wiki for this repo)?

Also there is one other project (a master's thesis) that I found which uses cubical Agda specifically: Univalent Categories.

By the way, that project was based on my old github.com/Saizan/cubical-demo it would be great if someone wanted to port it to this library instead.

from cubical.

@jashug has a paper using Cubical Agda (https://jashug.github.io/papers/ConstructingII.pdf, https://github.com/jashug/ConstructingII), although I believe it doesn't use univalence or HITs. (The motivation for using cubical type theory is to have function extensionality.)

from cubical.

Is something like the following provable? By coincidence it seems very close to the question that this issue started off with (with a little extra function-extensionality), but I'm still not seeing an answer.

{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude

pathExtensionality : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B} →
  isSet A → isSet B → (∀ (a : A) → transport p a ≡ transport q a) → p ≡ q
pathExtensionality iSA iSB w = ?

In particular, I'm trying to prove equal some paths which are all generated by isoToPath, by reasoning just about the forward parts of the underlying isomorphisms. A more direct way to do that would also be helpful. Thanks for any suggestions!

from cubical.

Here's a proof. You don't need to know that A and B are sets.

{-# OPTIONS --cubical --safe #-}
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence

pathExtensionality : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B}
  → (∀ (a : A) → transport p a ≡ transport q a) → p ≡ q
pathExtensionality {p = p} {q} w i =
  hcomp
    (λ j → λ
      { (i = i0) → secEq univalence p j
      ; (i = i1) → secEq univalence q j
      })
    (invEq univalence ((λ a → w a i) , t i))
  where
  t : PathP (λ i → isEquiv (λ a → w a i)) (pathToEquiv p .snd) (pathToEquiv q .snd)
  t = isProp→isContrPathP isPropIsEquiv (λ i a → w a i) _ _ .fst

If p and q come from isoToPath then there should be a more direct proof, but it seems to be something of a pain to write because isoToPath is not the same as ua ∘ isoToEquiv (or so Agda tells me, although I can't see the difference looking at the definitions...)

Nice @ecavallo ! I have a vague recollection that we discussed and proved this some time last year... Could you make a PR with this result so that we get it into the library?

from cubical.

If we have an equivalence e, what can we say about paths like secEq e x? It seems that they should be in some sense trivial (since they come from isEquiv and that is a proposition), but I have difficulty making that statement precise.

In my case e = f , _ is the equivalence between the below types Snat and SnatP and I have difficulty proving that ∀ n → secEq e (snat n) ≡ refl.

data Snat : Set where
  snat : ℕ → Snat
  snat-eq : ∀ m n → (e : Fin m ≃ Fin n) → snat m ≡ snat n

data SnatP : Set₁ where
  snat : ℕ → SnatP
  snat-eq : ∀ m n → (e : Fin m ≡ Fin n) → snat m ≡ snat n

f : Snat → SnatP
f (snat x) = snat x
f (snat-eq m n e i) = snat-eq m n (ua e) i

from cubical.

@ecavallo

isoToPath is not the same as ua ∘ isoToEquiv

I noticed this as well. I think it's because one of them is defined using copatterns and another is defined with a record expression. Maybe one of the definitions should be changed to match the other?

from cubical.

@Rotsor

If we have an equivalence e, what can we say about paths like secEq e x? It seems that they should be in some sense trivial (since they come from isEquiv and that is a proposition), but I have difficulty making that statement precise.

section (invEq e) (e .fst) is not a proposition in general, and so secEq e x is not uniquely determined. What we can say is that for an equivalence e : A ≃ B, the sigma type Σ[ g ∈ (B → A) ] (section g (e .fst)) is contractible. (This is one half of Lemma 4.2.9 in the HoTT book.)

It's often possible to project out non-propositional data from a proposition. For example, Σ[ n ∈ ℕ ] (n + n ≡ 4) is a proposition, but we can still get an element of ℕ (not a proposition) from it.

from cubical.

@ecavallo

isoToPath is not the same as ua ∘ isoToEquiv

I noticed this as well. I think it's because one of them is defined using copatterns and another is defined with a record expression. Maybe one of the definitions should be changed to match the other?

I agree

from cubical.

Btw we're moving to Gitter, see readme. It's a better place for discussion

from cubical.

(got confused about what was what, edited my last comment)

from cubical.

@ecavallo, thanks, that all makes sense now. A different choice of g can lead to a different choice of section _ _. It still seems that fixing a choice of g should uniquely determine the second component of the tuple, which I could somehow make use of. (but I'm still confused, as you can probably tell)

@ice1000, thanks. I'll look into that.

from cubical.

@ecavallo, maybe what I'm after is some property of isoToEquiv that relates the equivalence to the original isomorphism I built it from. Something like this:

module _ (A B : Set) (f : A → B) (g : B → A) sec ret where

  conj1 : secEq (isoToEquiv (iso f g ret sec)) ≡ sec
  conj1 = {!!}

  conj2 : retEq (isoToEquiv (iso f g ret sec)) ≡ ret
  conj2 = {!!}

Although I do realize that both of these can't be true, otherwise you'd be able to recover the original iso from the equivalence, which is not supposed to be possible. (probably wrong too)

(writing this here and not on gitter because it seems you're not on gitter)

from cubical.

Actually conj2 is satisfied with refl and conj1 might not hold in general.

from cubical.

Ok, by expanding the definitions and simplifying I have now this:

  conj3 : ∀ x → secEq e x ≡ ((sym (sec (g (f x)))) \∙ cong g (ret (f x))) \∙/ (refl ∙/ sec x)
  conj3 x = refl

(where _\∙/_, _∙/_, _\∙_ are variants of _∙_)

from cubical.

The proof worked, and conj3 is now called secEq-iso.

Is this the right way of doing things? If so, is secEq-iso worth having in the library?

from cubical.

While playing around with SIP and Escardó's excellent lecture notes, solving the exercises I noticed the following: Structures in his sense are families over types. Abstracting away the type-ness as a (one-higher) type with a suitable form of equivalence leads to the following definition of "universe" that is required for the proof to generalize, for details I prepared a gist

  record Universe {u} (UNIV : Type u) (e : Level) : Type (ℓ-max u (ℓ-suc e)) where
    field
      _≊_ : (S T : UNIV) → Type e
      id≊ : (S : UNIV) → S ≊ S
      ≡→≊ : ∀ {S T : UNIV} → (S ≡ T) → (S ≊ T)
      isEquiv≡→≊ : (S T : UNIV) → isEquiv (≡→≊ {S} {T})
      refl→id : ∀ {S} → ≡→≊ refl ≡ id≊ S

instantiating with the type universe and univalence should recover the current definition in Cubical.Foundations.SIP:

  TypeUniverse : {ℓ : Level} → Universe ℓ
  BigSIP.Universe._≊_ TypeUniverse = _≃_
  BigSIP.Universe.id≊ TypeUniverse = idEquiv
  BigSIP.Universe.≡→≊ TypeUniverse = univalence .fst
  BigSIP.Universe.isEquiv≡→≊ TypeUniverse _ _ = univalence .snd
  BigSIP.Universe.refl→id TypeUniverse = pathToEquivRefl

The important thing is we from a notion of structure on one universe of things gives us another universe, inhabited by certain structures on those things, with the equivalence in the bigger universe defined by sip:

module IteratedSIP {u} {UNIV : Type u} {e} {U : BigSIP.Universe UNIV e} where
  open BigSIP UNIV e
  open SIP U

  iteratedUniv : ∀ {s} {S : UNIV → Type s} {w} (σ : SNS S w)
               → BigSIP.Universe (Σ _ S) _
  BigSIP.Universe._≊_ (iteratedUniv σ) = _≃[ σ ]_
  BigSIP.Universe.id≊ (iteratedUniv σ) X = _ , idHomomorphism σ X
  BigSIP.Universe.≡→≊ (iteratedUniv σ) = characterization-of-≡ σ _ _  .fst
  BigSIP.Universe.isEquiv≡→≊ (iteratedUniv σ) A B = characterization-of-≡ σ A B .snd
  BigSIP.Universe.refl→id (iteratedUniv σ) = characterization-of-refl σ

References to published material is appreciated if anyone has any. Also, should I develop this into a pull request?

from cubical.

To add to the above, I have in the last few hours tried to use SIP (the extended one as outlined) in actual code, working out the correct path type for a more complicated structure. I have found that a modified version of the principle makes it easier for me. Instead of automatically providing a canonicalMap, let the user specify that + the proof that it's an equivalence, and also a proof that canonicalMap refl = idHomomorphism. It often makes it easier to proof the required equivalence since one has control over the exact implementation of the canonicalMap instead of being forced upon a transport wrapping it all. The strength is equivalent either way.

from cubical.

Yes. Regarding the last comment, this is already recorded here: canonical-map-equiv-criterion. Moreover, as recorded in canonical-map-equiv-criterion', it is enough to have any retraction, as such retractions are automatically equivalences.

from cubical.

The main point was that one can incrementally add structure and doesn't have to do that all in one go. As an example, the gist derives associative magmas by first doing magmas and then adding associativity - perhaps in a stylistically questionable way (could definitely use the second criterion to save some space), but hey it works :)

from cubical.

Closing this now that we have the stream on the Agda Zulip: https://agda.zulipchat.com/#narrow/stream/260790-cubical

from cubical.