9
$\begingroup$

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

$\endgroup$

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ I see, thank you! $\endgroup$ May 25 at 15:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.