I broadened the definition of extension-type-weakening (and all related terms) to allow the base type A to be a dependent family A : (t : ψ) → U rather than a static type.
This is a breaking change. I hope nobody (except me) is relying on those methods yet. If you are, it should hopefully be easy to adapt the code by invoking the constant family \ t -> A.
In any case, I think it is better to bite the bullet now rather than having to create a redundant second version of these methods later.
I broadened the definition of
extension-type-weakening(and all related terms) to allow the base typeAto be a dependent familyA : (t : ψ) → Urather than a static type.This is a breaking change. I hope nobody (except me) is relying on those methods yet. If you are, it should hopefully be easy to adapt the code by invoking the constant family
\ t -> A. In any case, I think it is better to bite the bullet now rather than having to create a redundant second version of these methods later.