Use #assume (alias of #variables) for extension extensionality

[fizruk]

This is only a minor suggestion, I'm happy to take feedback.

Currently, we use (extext : ExtExt) parameter in many definitions. However, we could instead use #variable and uses (...) notation to write as follows:

#lang rzk-1

-- Some definitions in this file rely on extension extensionality assumption
#variable extext : ExtExt

...

#def eq-ext-htpy uses (extext)
  ( I : CUBE)
  ( ψ : I -> TOPE)
  ( ϕ : ψ -> TOPE)
  ( A : ψ -> U)
  ( a : (t : ϕ) -> A t)
  ( f g : {t : I | ψ t} -> A t [ ϕ t |-> a t ])
  : ({t : I | ψ t} -> (f t = g t) [ ϕ t |-> refl ]) -> (f = g)
  := first (first (extext I ψ ϕ A a f g))

The benefit is that we do not need to pass extext explicitly and I think uses (extext) highlights this parameter as an assumption and distinguishes it from the regular parameters.

Note that rzk will issue an error if extext is used implicitly (and is not mentioned in uses (...)).

[emilyriehl]

This seems like an excellent suggestion to me. Should we treat funext similarly?

[fizruk]

Yes, I would treat all axioms this way, via global #variable declarations.

[fizruk]

Please, note that #assume is an alias for #variables. Perhaps, #assume is better for axioms.