Update Prelude.agda

[anshwad10]

make refl and lift instances

[mortberg]

What is the point of this PR? (I'm not so familiar with instances in Agda)

[anshwad10]

Instances in agda are basically a way to automate mechanical tasks. For example, take a look at how the 1lab uses instances to automatically calculate the hlevel of a type, allowing you to simply type hlevel! and solve the hlevel of a complicated type instead of manually using isSetPi2 IsSetSigma isSetSetQuotient isOfHLevelRespectEquiv blah blah blah. I made this PR, because earlier while using Cubical, I found myself needing an instance of Unit* which is Lift Unit, (even though there already is an instance of Unit), and I was surprised to find nobody had bothered to write the 3 lines of code needed to lift instances. And I also made refl an instance.

[felixwellen]

I think we should not make things instances in this way. It should be a decision of the user, to use instances or not. So if you want to make refl an instance for some reason, it should not be done in Prelude. Same for Data.Sigma. There should also be an example of a use case.

[felixwellen]

Just in case this is not clear: Before making an "open" (there is also a "draft" option) pull request, you should check your changes with agda.

[anshwad10]

What do you mean? It still will be the decision of the user to use instances or not. Making refl an instance won't affect the ability of the user to use it like a normal term in the way it has been used. It only allows Agda to find it in instance search. Same for lift. So this change is 100% backwards compatible.
As for a use case for instances, how about this:
Suppose you want to define the multiplicative inverse operation on rationals. Since it is a partial operation, it would look something like this:

module Example where

recip : (q : ℚ) → ¬ (q ≡ 0) → ℚ
recip q ¬q≡0 = {!!}

The problem with this definition is that whenever a user wants to apply recip to a concrete value, it has to provide a proof that it is nonzero, even though equality is decidable on Q so it could be automated. Now here is a version of this function that uses instances:

module Example where

recip' : (q : ℚ) {p : ¬ (q ≡ 0)} ⦃ _ : discreteℚ q 0 ≡ no p ⦄ → ℚ
recip' q {¬q≡0} = {!!}

Now when the user wants to compute, say, recip 2, they can just write that and the proof that 2 is nonzero is given automatically! (Note that this requires refl to be an instance, otherwise Agda would not find any instances and the operation would fail)
And what if the user wants to explicitly give the proof that q is nonzero (Perhaps when q is not a closed term, but some variable)? They can still do that!

recip : (q : ℚ) → ¬ (q ≡ 0) → ℚ
recip q ¬q≡0 = recip' q {¬q≡0} ⦃ ≡no _ _ ⦄

(here ≡no is a function in the library)

[felixwellen]

With "using instances" I meant that something is included in the instance search. I imagine it could be a problem to have to many instances at the same time. I would expect that it can get hard to figure out why some instance is not found by agda. Can you try to check the whole library with your changes?

[anshwad10]

I see, looks like adding a instance for Sigma is conflicting with its use in Cubical.Algebra.CommRing.Properties? So I should either enable --overlapping-instances or remove the Sigma instance altogether. However the refl and lift instances don't seem to be causing any problems, so we should keep those.

[anshwad10]

How do I type-check the library now?

[felixwellen]

I was adviced by agda developers to not use overlapping-instances, so I would only accept that, if there is a very good reason.
You can run make, see the instructions for contributing:
https://github.com/agda/cubical/blob/master/CONTRIBUTING.md

[anshwad10]

It looks like I have to have Agda installed on my computer to run make? If that's the case, I can't do that (I use Agdapad to code)

[felixwellen]

I think you should switch to an installed version of agda at this point.