How to access local definitions in Agda

Question

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 s:

I am trying to show sucℤ (predℤ f(x)) = x and I want to make the intermediate step of f(x)=x

Answer 1

You can refer to local definitions if the where block is declared as a module:

sucℤIso = iso sucℤ predℤ s r module Mod 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 

outer-s = Mod.s
outer-r = Mod.r

I often give the local module the same name as the function it's under. So we'd have module sucℤIso where here, and in the outer scope we can write:

outer-s = sucℤIso.s
outer-r = sucℤIso.r

Also note that a local where module is parameterized over all bound variables in local scope, and the local definitions are lifted out as functions. For example:

open import Data.Bool

f : Bool -> Bool
f x = y module f where
  y = true

f' : Bool -> Bool
f' = f.y

Here f.y is lifted out as a function with Bool -> Bool type.

Answer 2

To my knowledge this isn't possible, but you have a couple of options:

1. Declare s and r outside of sucℤIso. The where blocks are specifically local definitions: if you don't intend to only use it locally, don't declare it to be local.

2. For your specific case, you can use Iso.fun and Iso.inv to recover s and r from the isomorphism. Iso is just a record type, and iso is just a constructor (see here), so you can use the field projections fun and inv to recover the fields. So Iso.fun sucℤIso should yield s and Iso.inv sucℤIso should yield r.

   Note that this has nothing to do with the where clause, it's just because Iso is a record that you can project fields out of. If, for example, you just passed s and r to some function, there wouldn't always be a way to get them back.