Agda library encoding a free extension for the λ-calculus.
agda -i. Everything.agda
Categories
- Extensions to the
agda-category
libraryCategory.Instance.IndexedSetoids
- Category of setoids indexed by a set.
Data
- Extensions to the standard library
Empty.Irrel
- Irrelevant empty set for better propositional equality.
Vec.Membership.Reflexive
Vec
membership with propositional equality that doesn’t require axiom K.Vec.Relation.Unary.All.Ext
- Additional properties of
All
. Vec.Relation.Unary.All.Relation.Binary.Pointwise
- Pointwise relationship between dependent vectors.
LambdaFrex
- Core contributions of this library
Bundles
- Records to define λ-calculus models.
Category
- The category of λ-calculus models.
Terms
- Term algebra for the λ-calculus
Morphism
- Lift setoid functions to term algebra morphisms.
Properties
- Prove the term algebra forms the free functor.
Values
- Predicates for irreducible terms.
Types
- λ-calculus types and type contexts.