I'm working in cubical agda. I am wondering how to access local definitions once outside of the local environment. For example, suppose I have the following code:
sucℤIso : ℤ ≅ ℤ sucℤIso = iso sucℤ predℤ s r where s : section sucℤ predℤ s (pos zero) = refl s (pos (suc n)) = refl s (negsuc n) = refl r : retract sucℤ predℤ r (pos n) = refl r (negsuc zero) = refl r (negsuc (suc n)) = refl
Now, later on, I want to use
s and apply it to something. Does anybody know how to do this?
Here are the details of how I am trying to use
I am trying to show
sucℤ (predℤ f(x)) = x and I want to make the intermediate step of