search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.41k stars 339 forks source link

Normalization gives trivial `transp` #7312

Closed Trebor-Huang closed 2 weeks ago

Trebor-Huang commented 2 weeks ago

Consider the following code

{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Bool
open import Cubical.Data.Sigma
a = transp (λ i → Bool × ℕ) i0 (true , 3)
_ : a ≡ (true , 3)
_ = refl

Agda correctly recognizes a = (true , 3), but using the VSCode plugin to normalize a via C-c C-n, I get transp (λ i → Σ Bool (λ _ → ℕ)) i0 (true , 3) back. Why is this happening? In my actual case there's like hundreds of trivial transp stacked on the actual result, and I can't read anything.

plt-amy commented 2 weeks ago

Because transp on record types only computes when projected from; you can normalise projectionwise to see what each field computes to. More generally, reflexive transports should not be expected to reduce to the base in general (or quantified-over) types, and we exploit this to reduce the sizes of normal forms, particularly when eta-expansion applies. Transport doesn't eagerly reduce on functions or paths, either (you have to apply them).