pi package:Agda

Dependent function space Γ → A.

ex: (xs:e) -> e or {xs:e} -> e

dependent or non-dependent function space

Does a function space need brackets?

piAbstract (v, a) b[v] = (w : a) -> b[w]

For the inspect idiom, it does something special: @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> b[w] For rewrite, it does something special: piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']

piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w] piAbstractTerm Hidden v a b[v] = {w : a} -> b[w]

(x:A)->B(x) piApply [u] = B(u)

Precondition: The type must contain the right number of pis without having to perform any reduction. piApply is potentially unsafe, the monadic piApplyM is preferable.

Compute the sort of a pi type from the sorts of its domain and codomain. This function should only be called on reduced sorts, since the LevelUniv rules should only apply when the sort doesn't reduce to Set

Returns Left (a,b) in case the type is Pi a b or PathP b _ _. Assumes the Type is in whnf.

Collect A.Pis.

Sort of the pi type.

Dependent function types. The domain will be represented accurately, for the case of a genuine dependent function type, the codomain will be a dummy.