Skip to content
Agda-Pages Demo
Library
Initializing search
agda-pages-demo
Home
Demo
Library
Tags
Agda-Pages Demo
agda-pages-demo
Home
Demo
Demo
Hierarchy
Hierarchy
Sub
Sub
Base
Literate
Literate
LaTeX
Markdown
Metadata
Plain
Plain
hello-world-dep
hello-world-dep-lookup
Search
Search
Characters
Space
Space
LaTeX
Markdown
Library
Library
Agda
Agda
Builtin
Builtin
Bool
Equality
List
Maybe
Nat
Sigma
Unit
Primitive
Algebra
Algebra
Bundles
Bundles
Raw
Consequences
Consequences
Base
Propositional
Setoid
Construct
Construct
LiftedChoice
NaturalChoice
NaturalChoice
Base
Max
MaxOp
Min
MinMaxOp
MinOp
Core
Definitions
Definitions
RawMagma
Lattice
Lattice
Bundles
Bundles
Raw
Construct
Construct
NaturalChoice
NaturalChoice
MaxOp
MinMaxOp
MinOp
Properties
Properties
BooleanAlgebra
DistributiveLattice
Lattice
Semilattice
Structures
Morphism
Morphism
Definitions
Structures
Properties
Properties
CommutativeSemigroup
Semigroup
Structures
Structures
Biased
Axiom
Axiom
Extensionality
Extensionality
Propositional
UniquenessOfIdentityProofs
Data
Data
Bool
Bool
Base
ListAction
Properties
Empty
Empty
Polymorphic
Fin
Fin
Base
Patterns
Properties
Irrelevant
List
List
Base
Effectful
Extrema
Extrema
Core
Membership
Membership
Propositional
Propositional
Properties
Properties
Core
Setoid
Setoid
Properties
Properties
Relation
Relation
Binary
Binary
Equality
Equality
Propositional
Setoid
Pointwise
Pointwise
Base
Properties
Subset
Subset
Propositional
Setoid
Unary
Unary
All
All
Properties
Properties
Core
AllPairs
AllPairs
Core
Any
Any
Properties
Unique
Unique
Setoid
Maybe
Maybe
Base
Relation
Relation
Unary
Unary
All
Any
Nat
Nat
Base
Divisibility
Divisibility
Core
DivMod
DivMod
Core
GeneralisedArithmetic
Induction
Properties
Parity
Parity
Base
Product
Product
Algebra
Base
Function
Function
Dependent
Dependent
Propositional
NonDependent
NonDependent
Propositional
Setoid
Properties
Relation
Relation
Binary
Binary
Pointwise
Pointwise
NonDependent
Unary
Unary
All
Sign
Sign
Base
Sum
Sum
Algebra
Base
Function
Function
Propositional
Setoid
Properties
Relation
Relation
Binary
Binary
Pointwise
These
These
Base
Unit
Unit
Base
Polymorphic
Polymorphic
Base
Properties
Vec
Vec
Base
Bounded
Bounded
Base
Effect
Effect
Applicative
Choice
Empty
Functor
Monad
Function
Function
Base
Bundles
Consequences
Consequences
Propositional
Setoid
Construct
Construct
Composition
Identity
Symmetry
Core
Definitions
Dependent
Dependent
Bundles
Indexed
Indexed
Relation
Relation
Binary
Binary
Equality
Metric
Metric
Bundles
Core
Definitions
Nat
Nat
Bundles
Core
Definitions
Structures
Structures
Properties
Properties
Bijection
Inverse
Inverse
HalfAdjointEquivalence
RightInverse
Surjection
Related
Related
Propositional
TypeIsomorphisms
Structures
Induction
Induction
WellFounded
Level
Relation
Relation
Binary
Binary
Bundles
Bundles
Raw
Consequences
Construct
Construct
Composition
Flip
Flip
EqAndOrd
Intersection
NaturalOrder
NaturalOrder
Left
NonStrictToStrict
Core
Definitions
Indexed
Indexed
Heterogeneous
Heterogeneous
Bundles
Construct
Construct
Trivial
Core
Definitions
Structures
Lattice
Lattice
Bundles
Definitions
Structures
Morphism
Morphism
Definitions
Structures
Properties
Properties
DecTotalOrder
Poset
Preorder
Setoid
TotalOrder
PropositionalEquality
PropositionalEquality
Algebra
Core
Properties
Reasoning
Reasoning
Base
Base
Double
Single
Triple
Preorder
Setoid
Syntax
Structures
Structures
Biased
Nullary
Nullary
Decidable
Decidable
Core
Indexed
Irrelevant
Negation
Negation
Core
Recomputable
Recomputable
Core
Reflects
Unary
Unary
PredicateTransformer
Properties
Tags
Home
Library
Library
Info
All imported Agda library modules are automatically included in this section.
Back to top