nLab
Agda

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

judgement
hypothetical judgement, sequent
- antecedents $\vdash$ consequent, succedents

type theory (dependent, intensional, observational type theory, homotopy type theory)

calculus of constructions

syntax object language

theory, axiom
proposition/type (propositions as types)
definition/proof/program (proofs as programs)
theorem

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logic	category theory	type theory
true	terminal object/(-2)-truncated object	h-level 0-type/unit type
false	initial object	empty type
proposition	(-1)-truncated object	h-proposition, mere proposition
proof	generalized element	program
cut rule	composition of classifying morphisms / pullback of display maps	substitution
cut elimination for implication	counit for hom-tensor adjunction	beta reduction
introduction rule for implication	unit for hom-tensor adjunction	eta conversion
logical conjunction	product	product type
disjunction	coproduct ((-1)-truncation of)	sum type (bracket type of)
implication	internal hom	function type
negation	internal hom into initial object	function type into empty type
universal quantification	dependent product	dependent product type
existential quantification	dependent sum ((-1)-truncation of)	dependent sum type (bracket type of)
equivalence	path space object	identity type
equivalence class	quotient	quotient type
induction	colimit	inductive type, W-type, M-type
higher induction	higher colimit	higher inductive type
completely presented set	discrete object/0-truncated object	h-level 2-type/preset/h-set
set	internal 0-groupoid	Bishop set/setoid
universe	object classifier	type of types
modality	closure operator, (idemponent) monad	modal type theory, monad (in computer science)
linear logic	(symmetric, closed) monoidal category	linear type theory/quantum computation
proof net	string diagram	quantum circuit
(absence of) contraction rule	(absence of) diagonal	no-cloning theorem
	synthetic mathematics	domain specific embedded programming language

homotopy levels

semantics

Edit this sidebar

Overview
Related concepts
References

Overview

A dependently typed functional programming language with applications to certified programming. It is also used as a proof assistant.

Besides Coq, Agda is one of the languages in which homotopy type theory has been implemented (Brunerie). Agda can be compiled to Haskell, Epic or Javascript.

Related concepts

proof assistants:

based on plain type theory/set theory:

Metamath
Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

Coq, Agda, Lean, Arend

For higher category theory:

projects for formalization of mathematics with proof assistants:

Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
MathScheme
UniMath project (using Coq)
Xena project (using Lean)

Historical projects that died out:

The QED Project

References

General information on Agda is at

Agda Wiki
‘Hello World!’ in Adga
learn-you-an-agda (and achieve enlightment)
Ulf Norell, James Chapman, Dependently Typed Programming in Agda (pdf)
Dan Licata, Ian Voysey, Programming and proving in Agda
Ulf Norell, Towards a practical programming

language based on dependent type theory_, 2007 (pdf)

A tutorial for use of Agda as an implementation of homotopy type theory is at

Guillaume Brunerie, Agda for homotopy type theory (web)
Guillaume Brunerie, The Agda proof assistant, slides, pdf

and specifically of Cubical Agda as an implementation of cubical type theory:

Andrea Vezzosi, Anders Mörtberg and Andreas Abel, Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, 2019 (pdf)

The HoTT-Agda library is at

github, hott-agda

category: software

Last revised on September 12, 2019 at 03:04:06. See the history of this page for a list of all contributions to it.

nLab Agda