| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Telescope.Path
Documentation
telePiPath :: (Abs Type -> Abs Type) -> Telescope -> Type -> Boundary -> TCM Type Source #
In an ambient context Γ, telePiPath f Δ t bs builds a type that
can be telViewPathBoundaryP'ed into (TelV Δ t, bs').
Γ.Δ ⊢ t
bs = [(i,u_i)]
Δ = Δ0,(i : I),Δ1
∀ b ∈ {0,1}. Γ.Δ0 | u_i .b : (telePiPath f Δ1 t bs)(i = b)
Γ ⊢ telePiPath f Δ t bs