Agda
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.Record.Cubical

Documentation

addCompositionForRecord Source #

Arguments

:: QName

Datatype name.

-> EtaEquality 
-> ConHead 
-> Telescope

Γ parameters.

-> [Arg QName]

Projection names.

-> Telescope

Γ ⊢ Φ field types.

-> Type

Γ ⊢ T target type.

-> TCM ()