nLab
judgmental equality
Contents
Context
Type theory
natural deduction metalanguage, practical foundations
 type formation rule
 term introduction rule
 term elimination rule
 computation rule
type theory (dependent, intensional, observational type theory, homotopy type theory)
syntax object language
= + +
  

 /  / 
  
  , 
  
 of / of  
for  for homtensor adjunction  
introduction rule for  for homtensor adjunction  
  
 ( of)  ( of) 
  
 into  into 
  
 ( of)  ( of) 
  
  
  , , 
higher   
 /  // 
  / 
  
 , ()  , 
 (, )  / 
  
(absence of)  (absence of)  
  
homotopy levels
semantics
Equality and Equivalence
equivalence

equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)

identity type, equivalence in homotopy type theory

isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)category

natural equivalence, natural isomorphism

gauge equivalence

Examples.
principle of equivalence
equation

fiber product, pullback

homotopy pullback

Examples.

linear equation, differential equation, ordinary differential equation, critical locus

EulerLagrange equation, Einstein equation, wave equation

Schrödinger equation, KnizhnikZamolodchikov equation, MaurerCartan equation, quantum master equation, EulerArnold equation, Fuchsian equation, FokkerPlanck equation, Lax equation
Contents
Idea
A notion of equality in type theory involving the notion of judgement.
References

Robin Adams, Pure type systems with judgemental equality, Journal of Functional Programming, Volume 16 Issue 2(2006) (web)

Vincent Siles, Hugo Herbelin, Equality is typable in semifull pure type systems (pdf)
Created on September 18, 2012 at 21:32:22.
See the history of this page for a list of all contributions to it.