A better name for `cong`? about cubical HOT 14 CLOSED

I wouldn't rename it just because it would make things a bit confusing for anyone who's coming from standard Agda. It might be worth it to add a comment about this though (even though it is clear if you look at the code :-) )

from cubical.

I don't know about anyone else, but I'd still like to have _∘_ be general function composition.

from cubical.

Maybe not rename it but when you experiment with Agda you can do something like _$_ for cong. If you define precedence right it may save you quite a few brackets (so instead of cong f (cong g (complicated p)) you can have f $ g $ complicated p)

from cubical.

Maybe not rename it but when you experiment with Agda you can do something like _$_ for cong. If you define precedence right it may save you quite a few brackets (so instead of cong f (cong g (complicated p)) you can have f $ g $ complicated p)

cong has a very direct proof in Cubical Agda and I like to inline it. Your example would then be \ i -> f (g (complicated p i)). Still quite a few parantheses, but you don't need to write cong.

from cubical.

cong has a very direct proof in Cubical Agda and I like to inline it. Your example would then be \ i -> f (g (complicated p i)). Still quite a few parantheses, but you don't need to write cong.

Ah good point. I really wish compPath can be easily inline as well.

from cubical.

Maybe we should have another name for compPath... Like semicolon or just a dot.

from cubical.

Maybe we should have another name for compPath... Like semicolon or just a dot.

Yeah that sounds like a good idea! _∙_ (Enter ∙ by \.) should be good.

BTW I just tried inline some of the proofs but once inlined Agda complains about Termination checking failed. Is this a known issue?

This is the one I tried: (https://github.com/agda/cubical/blob/master/Cubical/Data/Int/Properties.agda#L268)

{-                                                                                                                       
minusPlus (negsuc (suc m)) n =                                                                                           
  predInt (sucInt (sucInt (n +pos m)) +negsuc m) ≡⟨ predInt+negsuc m (sucInt (sucInt (n +pos m))) ⟩                                                                      
  predInt (sucInt (sucInt (n +pos m))) +negsuc m ≡⟨ cong (λ z → z + negsuc m) (predSuc (sucInt (n +pos m))) ⟩                                                            
  sucInt (n +pos m) +negsuc m                    ≡⟨ minusPlus (negsuc m) n ⟩                                             
  n ∎                                                                                                                    
-}

minusPlus (negsuc (suc m)) n i =
  hcomp (λ j → \ { (i = i0) → (predInt+negsuc m (sucInt (sucInt (n +pos m))) (~ j))
                 ; (i = i1) → minusPlus (negsuc m) n j }) (predSuc (sucInt (n +pos m)) i + negsuc m)

Using the commented version is fine. But using the uncommented one, it complains.

from cubical.

@3abc I've noticed before that the termination checker doesn't deal well with pattern matching lambdas, at least ones used for systems. I wonder if making it its own definition helps.

I really like the idea of defining _∙_ as a synonym for compPath btw.

from cubical.

I really like the idea of defining _∙_ as a synonym for compPath btw.

What will be a good fixity for _∙_?

I suggest Infix, and higher than function application. I wish one can write λ i → f p∙q i for cong f (compPath p q) without having to write parentheses.

BTW currently λ i → p i doesn't fit well with equational reasoning: ≡⟨ λ i → f p i ⟩ won't work, one have to do ≡⟨ (λ i → f p i) ⟩, so sometimes it still make sense to write ≡⟨ cong f p ⟩ instead of inline it.

from cubical.

I suggest Infix, and higher than function application. I wish one can write λ i → f p∙q i for cong f (compPath p q) without having to write parentheses.

I think of path composition as multiplication (in the groupoid of paths) so having it bind harder than function application is very confusing (consider λ i → f p ∙ q i)

from cubical.

BTW currently λ i → p i doesn't fit well with equational reasoning: ≡⟨ λ i → f p i ⟩ won't work, one have to do ≡⟨ (λ i → f p i) ⟩, so sometimes it still make sense to write ≡⟨ cong f p ⟩ instead of inline it.

If one can fix this by changing the fixity of the eq reasoning that would be nice. I just copied the current setup from the standard library without thinking about it. I'm in fact allergic to thinking about fixity, so I would be happy if someone else wants to play around with it :-)

from cubical.

Lambdas are quite special, so I don't think fixities can solve this.

However we can have special syntax for equality reasoning that binds the i.
Then it could look like ≡λ i ↦ f p i ⟩ or so.

from cubical.

I think of path composition as multiplication (in the groupoid of paths) so having it bind harder than function application is very confusing (consider λ i → f p ∙ q i)

Yeah I think of it that way too. Maybe λ i → f (p ∙ q) i is good enough.

from cubical.

However we can have special syntax for equality reasoning that binds the i.
Then it could look like ≡λ i ↦ f p i ⟩ or so.

Actually I found that the reason of wanting some syntactic sugar for cong is sometimes in equational reasoning, having to keep writing cong and a function is annoying, like

longFunction x ≡⟨ cong longFunction p ⟩
longFunction y ≡⟨ cong longFunction q ⟩
longFunction z ≡⟨ cong longFunction r ⟩
longFunction t ≡⟨ ... ⟩
_ ∎

especially when p, q, r are complicated too. However I just realized these can be written as

longFunction x ≡⟨ cong longFunction (
  x ≡⟨ p ⟩
  y ≡⟨ q ⟩
  z ≡⟨ r ⟩
  t ∎ ) ⟩
longFunction t ≡⟨ ... ⟩
_ ∎

so I'm happy with cong for now.

from cubical.