LogRel.Utils: basic generically useful definitions, notations, tactics…

LogRel.BasicAst: definitions preceding those of the AST of terms: sorts, binder annotations…

LogRel.AutoSubst.core

LogRel.AutoSubst.unscoped

LogRel.AutoSubst.Ast

LogRel.AutoSubst.Extra: extra content to better handle the boilerplate generated by AutoSubst.

LogRel.Context: definition of contexts and operations on them.

LogRel.Notations: notations for conversion, typing and the logical relations.

LogRel.Computation: internal definitions related to the computation model.

LogRel.Closed

LogRel.NormalForms: definition of normal and neutral forms, and properties.

LogRel.Weakening: definition of well-formed weakenings, and some properties.

LogRel.NormalEq

LogRel.UntypedReduction: untyped reduction, used to define algorithmic typing.

LogRel.Confluence

LogRel.Standardisation

LogRel.GenericTyping: the generic interface of typing used to build the logical relation.

LogRel.DeclarativeTyping: specification of conversion and typing, in a declarative fashion.

LogRel.DeclarativeInstance: proof that declarative typing is an instance of generic typing.

LogRel.DeepTyping

LogRel.LogicalRelation: Definition of the logical relation

LogRel.LogicalRelation.Induction: good induction principles for the logical relation.

LogRel.LogicalRelation.Escape: the logical relation implies conversion/typing.

LogRel.LogicalRelation.ShapeView: relating reducibility witnesses of reducibly convertible types.

LogRel.LogicalRelation.Reflexivity: reflexivity of the logical relation.

LogRel.LogicalRelation.Irrelevance: symmetry and irrelevance of the logical relation.

LogRel.LogicalRelation.Weakening

LogRel.LogicalRelation.Universe

LogRel.LogicalRelation.Neutral

LogRel.LogicalRelation.Transitivity

LogRel.LogicalRelation.Reduction

LogRel.LogicalRelation.NormalRed

LogRel.LogicalRelation.Application

LogRel.LogicalRelation.SimpleArr

LogRel.LogicalRelation.Id

LogRel.Validity

LogRel.Substitution.Irrelevance

LogRel.Substitution.Properties

LogRel.Substitution.Escape

LogRel.Substitution.Conversion

LogRel.Substitution.Reflexivity

LogRel.Substitution.Reduction

LogRel.Substitution.SingleSubst

LogRel.Substitution.Introductions.Application

LogRel.Substitution.Introductions.Universe

LogRel.Substitution.Introductions.Poly

LogRel.Substitution.Introductions.Pi

LogRel.Substitution.Introductions.Lambda

LogRel.Substitution.Introductions.SimpleArr

LogRel.Substitution.Introductions.Var

LogRel.Substitution.Introductions.Nat

LogRel.Substitution.Introductions.Empty

LogRel.Substitution.Introductions.Sigma

LogRel.Substitution.Introductions.Id

LogRel.Substitution.Introductions.Quote

LogRel.Substitution.Introductions.Reflect

LogRel.Fundamental: declarative typing implies the logical relation for any generic instance.

LogRel.DeclarativeSubst: stability of declarative typing by substitution.

LogRel.TypeConstructorsInj: injectivity and no-confusion of type constructors, and many consequences, including subject reduction.

LogRel.Consequences: important meta-theoretic consequences of normalization: canonicity of natural numbers and consistency.

LogRel.Main