Library MetaCoq.Checker.All
Library MetaCoq.Checker.Closed
Library MetaCoq.Checker.Extraction
Library MetaCoq.Checker.Generation
Library MetaCoq.Checker.LibHypsNaming
Library MetaCoq.Checker.Loader
Library MetaCoq.Checker.MetaTheory
Library MetaCoq.Checker.Normal
Library MetaCoq.Checker.Retyping
Library MetaCoq.Checker.Substitution
Library MetaCoq.Checker.Typing
- Typing derivations
- Lemmas about All_local_env
Library MetaCoq.Checker.TypingWf
Library MetaCoq.Checker.WcbvEval
Library MetaCoq.Checker.Weakening
Library MetaCoq.Checker.WeakeningEnv
Library MetaCoq.Checker.WfInv
Library MetaCoq.Checker.uGraph
Library MetaCoq.Checker.wGraph
Library MetaCoq.Erasure.EAll
Library MetaCoq.Erasure.EArities
Library MetaCoq.Erasure.EAst
Library MetaCoq.Erasure.EAstUtils
Library MetaCoq.Erasure.EInduction
Library MetaCoq.Erasure.EInversion
Library MetaCoq.Erasure.ELiftSubst
Library MetaCoq.Erasure.EPretty
Library MetaCoq.Erasure.ESubstitution
Library MetaCoq.Erasure.ETyping
Library MetaCoq.Erasure.EWcbvEval
Library MetaCoq.Erasure.EWndEval
Library MetaCoq.Erasure.ErasureCorrectness
Library MetaCoq.Erasure.ErasureFunction
Library MetaCoq.Erasure.Extract
Library MetaCoq.Erasure.Extraction
Library MetaCoq.Erasure.Loader
Library MetaCoq.Erasure.Prelim
Library MetaCoq.Erasure.SafeErasureFunction
Library MetaCoq.Erasure.SafeTemplateErasure
Library MetaCoq.PCUIC.Extraction
Library MetaCoq.PCUIC.PCUICAll
Library MetaCoq.PCUIC.PCUICAlpha
Library MetaCoq.PCUIC.PCUICAst
Library MetaCoq.PCUIC.PCUICAstUtils
Library MetaCoq.PCUIC.PCUICChecker
Library MetaCoq.PCUIC.PCUICCheckerCompleteness
Library MetaCoq.PCUIC.PCUICClosed
Library MetaCoq.PCUIC.PCUICConfluence
Library MetaCoq.PCUIC.PCUICContextConversion
Library MetaCoq.PCUIC.PCUICConversion
Library MetaCoq.PCUIC.PCUICCumulativity
Library MetaCoq.PCUIC.PCUICElimination
Library MetaCoq.PCUIC.PCUICEquality
Library MetaCoq.PCUIC.PCUICErasedTerm
Library MetaCoq.PCUIC.PCUICGeneration
Library MetaCoq.PCUIC.PCUICInduction
Library MetaCoq.PCUIC.PCUICInversion
Library MetaCoq.PCUIC.PCUICLiftSubst
Library MetaCoq.PCUIC.PCUICLoader
Library MetaCoq.PCUIC.PCUICMetaTheory
Library MetaCoq.PCUIC.PCUICNameless
Library MetaCoq.PCUIC.PCUICNormal
Library MetaCoq.PCUIC.PCUICParallelReduction
Library MetaCoq.PCUIC.PCUICParallelReductionConfluence
Library MetaCoq.PCUIC.PCUICPosition
Library MetaCoq.PCUIC.PCUICPretty
Library MetaCoq.PCUIC.PCUICPrincipality
Library MetaCoq.PCUIC.PCUICReduction
Library MetaCoq.PCUIC.PCUICReflect
Library MetaCoq.PCUIC.PCUICRetyping
Library MetaCoq.PCUIC.PCUICSN
Library MetaCoq.PCUIC.PCUICSR
Library MetaCoq.PCUIC.PCUICSafeLemmata
Library MetaCoq.PCUIC.PCUICSigmaCalculus
Library MetaCoq.PCUIC.PCUICSize
Library MetaCoq.PCUIC.PCUICSubstitution
Library MetaCoq.PCUIC.PCUICTyping
- Typing derivations
- Lemmas about All_local_env
Library MetaCoq.PCUIC.PCUICUnivSubst
Library MetaCoq.PCUIC.PCUICUnivSubstitution
Library MetaCoq.PCUIC.PCUICValidity
Library MetaCoq.PCUIC.PCUICWcbvEval
Library MetaCoq.PCUIC.PCUICWeakening
Library MetaCoq.PCUIC.PCUICWeakeningEnv
Library MetaCoq.PCUIC.TemplateToPCUIC
Library MetaCoq.PCUIC.TemplateToPCUICCorrectness
Library MetaCoq.SafeChecker.Extraction
Library MetaCoq.SafeChecker.Loader
Library MetaCoq.SafeChecker.PCUICSafeChecker
Library MetaCoq.SafeChecker.PCUICSafeConversion
Library MetaCoq.SafeChecker.PCUICSafeReduce
Library MetaCoq.SafeChecker.PCUICSafeRetyping
Library MetaCoq.SafeChecker.SafeTemplateChecker
Library MetaCoq.Template.All
Library MetaCoq.Template.Ast
Library MetaCoq.Template.AstUtils
Library MetaCoq.Template.BasicAst
Library MetaCoq.Template.ExtractableLoader
Library MetaCoq.Template.Extraction
Library MetaCoq.Template.Induction
Library MetaCoq.Template.LiftSubst
Library MetaCoq.Template.Loader
Library MetaCoq.Template.Pretty
Library MetaCoq.Template.TemplateMonad
Library MetaCoq.Template.UnivSubst
Library MetaCoq.Template.Universes
Library MetaCoq.Template.config
Library MetaCoq.Template.monad_utils
Library MetaCoq.Template.utils
Library MetaCoq.Translations.MiniHoTT
- Path operations are equivalences
- Universal mapping property
- Paths
- Path algebra
- Transport
- Maps on paths
- Dependent paths
- Functorial action
- Equivalences
- Truncatedness: any dependent product of n-types is an n-type
- Contractibility: A product over a contractible type is equivalent to the fiber over the center.
- Symmetry of curried arguments
- Unpacking
- Eta conversion
- Paths
- Transport
- Functorial action
- Equivalences
- Associativity
Library MetaCoq.Translations.MiniHoTT_paths
- Path operations are equivalences
- Universal mapping property
- Paths
- Path algebra
- Transport
- Maps on paths
- Dependent paths
- Functorial action
- Equivalences
- Truncatedness: any dependent product of n-types is an n-type
- Contractibility: A product over a contractible type is equivalent to the fiber over the center.
- Symmetry of curried arguments
- Unpacking
- Eta conversion
- Paths
- Transport
- Functorial action
- Equivalences
- Associativity
Library MetaCoq.Translations.param_cheap_packed
Library MetaCoq.Translations.param_cheap_packed_correctness
Library MetaCoq.Translations.param_generous_packed
Library MetaCoq.Translations.param_generous_packed_correctness
Library MetaCoq.Translations.param_generous_unpacked
Library MetaCoq.Translations.param_original
Library MetaCoq.Translations.sigma
Library MetaCoq.Translations.standard_model
Library MetaCoq.Translations.times_bool_fun
Library MetaCoq.Translations.times_bool_fun2
Library MetaCoq.Translations.translation_utils
This page has been generated by coqdoc