agdadependent-type

Agda: is there a way to use the information provided by with-abstraction in the function definition?

I'm trying to construct the lattice of intervals with the datatype defined as follows:

data 𝕀 : Set where
  ⊀   : 𝕀
  βŠ₯   : 𝕀
  -∞  : β„€ β†’ 𝕀
  _+∞ : β„€ β†’ 𝕀
  I   : (l : β„€) β†’ (u : β„€) β†’ {l ≀ u} β†’ 𝕀

in order to define the βŠ“π•€ (glb) operator over intervals in some cases I'd have to pattern match over i ≀ᡇ j to define the appropriate value of the operator, although I'm not sure how I can reuse the information provided by the pattern matching in the case definition.

In particular in the case

-∞ x βŠ“π•€ (y +∞) with (y ≀ᡇ x) | inspect (y ≀ᡇ_) x
... | false | [ y≀x≑ff ] = βŠ₯
... | true | [ y≀x≑tt ] = I y x {≀ᡇ⇒≀ {!!}}

I have a witness that (y ≀ᡇ x) ≑ true but I'm not sure on how to use it to combine it with ≀ᡇ⇒≀ in order to produce the witness of y ≀ x

Solution

  • Use _≀?_ instead:

    open import Relation.Nullary.Decidable.Core

_βŠ“π•€_ : 𝕀 β†’ 𝕀 β†’ 𝕀
-∞ x βŠ“π•€ (y +∞) with y ≀? x
... | yes y≀x = I y x {y≀x}
... | no _ = βŠ₯

    To answer your question literally, you can use T-≑: ≀ᡇ⇒≀ (Equivalence.from T-≑ y≀x≑tt).