|
[{"tag":"Heading","contents":[0,"Martin-Löf Type Theory"]},{"tag":"Paragraph","contents":"A description of Martin-Löf Type Theory in Holbert, by Brendan Zabarauskas."},{"tag":"Paragraph","contents":"Original gist: ~https://gist.github.com/brendanzab/1b4732179b15201bf33fed6dbca02458~"},{"tag":"Heading","contents":[2,"Introduction"]},{"tag":"Paragraph","contents":"/Martin-Löf Type Theory/ (MLTT), also known as /Intuitionistic Type Theory/, is a type theory proposed by Per Martin-Löf in the mid 70s. It forms the basis of many popular dependently typed programming languages and theorem provers, for example Agda, Coq, Idris, Epigram, and more. The influence of MLTT also extends to other languages, for example partly inspiring the module systems of Standard ML and OCaml, and in the work on adding dependent types to Haskell."},{"tag":"Paragraph","contents":"The main forms of judgement in this presentation of Martin-Löf Type theory are:\n\n- $A:_type A$\n which can be read as “$A:A$ is a type”\n\n- $A a:_:_ a A$\n which can be read as “$a:a$ is an expression of type $A:A$”\n\n- $A1 A2:_==_type A1 A2$\n which can be read as “$A1:A1$ and $A2:A2$ are definitionally equal types”\n\n- $A a1 a2:_==_:_ a1 a2 A$\n which can be read as “$a1:a1$ and $a2:a2$ are definitionally equal expressions of type $A:A$”"},{"tag":"Paragraph","contents":"The type theory is described /declaratively/ as opposed to /algorithmically/. For example the symmetry rule for the definitional equality judgement could be applied an arbitrary number of times! These rules need to be restricted in order to describe a tractable type checking algorithm for a real-world implementation. This might involve restricting the equality rules, and also making the algorithm /bidirectional/, splitting the rules into /checking/ and /synthesis/ modes."},{"tag":"Paragraph","contents":"*Warning*: I'm not a type theory expert, nor am I a logician, so I've probably messed up in a number of places. Let me know if you find any issues, but please proceed with skepticism – this was mainly intended to be a fun experiment! :)"},{"tag":"Heading","contents":[2,"Resources"]},{"tag":"Paragraph","contents":"- D. P. Friedman, and D. T. Christiansen, “The Little Typer”\n ~https://mitpress.mit.edu/books/little-typer~\n- Z. Luo, “Notes on Universes in Type Theory”\n ~https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf~\n- B. Nordström, K. Petersson, and J. M. Smith. “Programming in Martin-Löf’s Type Theory”\n ~https://www.cse.chalmers.se/research/group/logic/book/book.pdf~"},{"tag":"Heading","contents":[2,"Definitional Equality"]},{"tag":"Paragraph","contents":"Definitional equality is reflexive, symmetric and transitive."},{"tag":"Heading","contents":[3,"Reflexixity"]},{"tag":"Paragraph","contents":"We can treat types and terms as the same as themselves through the use of the /reflexivity/ rules for definitional equality."},{"tag":"Rule","contents":["Axiom",[["equal-type/refl",[["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}],null],["equal-term/refl",[["A","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}],null]],[]]},{"tag":"Heading","contents":[3,"Symmetry"]},{"tag":"Paragraph","contents":"Two sides of a definitional equality judgement can be swapped thanks to the /symmetry/ rules. This greatly cuts down on the number of rules we’ll need to define for the type connectives we’ll be defining later on."},{"tag":"Rule","contents":["Axiom",[["equal-type/symm",[["A1","A2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}],null],["equal-term/symm",[["A","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":2}]}],null]],[]]},{"tag":"Heading","contents":[3,"Transitivity"]},{"tag":"Paragraph","contents":"We can connect together two definitional equality judgements through the use of the /transitivity/ rules."},{"tag":"Rule","contents":["Axiom",[["equal-type/trans",[["A1","A2","A3"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}],null],["equal-term/trans",[["A","a1","a2","a3"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":3}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}],null]],[]]},{"tag":"Heading","contents":[3,"Type Equality"]},{"tag":"Paragraph","contents":"The following rules relate to how definitional equality is handled in types."},{"tag":"Rule","contents":["Axiom",[["term/equal-type",[["A1","A2","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}],null],["equal-term/equal-type",[["A1","A2","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}],null]],[]]},{"tag":"Heading","contents":[2,"Dependent Function Types"]},{"tag":"Paragraph","contents":"Dependent function types are function types where the type of the output depends on input that was applied. These are also known as ‘dependent product types’, which is where the $Pi$ notation comes from."},{"tag":"Heading","contents":[3,"Statics"]},{"tag":"Rule","contents":["Axiom",[["function/formation",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["function/introduction",[["A","B","b"],[[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["function/elimination",[["A","B","f","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Dynamics"]},{"tag":"Rule","contents":["Axiom",[["function/equal( Pi__)",[["A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["function/equal( lambda_)",[["A","B","b1","b2"],[[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["function/equal(apply__)",[["A","B","f1","f2","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":5}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":5}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":4},{"tag":"LocalVar","contents":1}]}]}],null],["function/computation(apply( lambda_)_)",[["A","B","f1","f2","a1","a2","b"],[[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":7}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":4},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":6},{"tag":"LocalVar","contents":0}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":6}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"LocalVar","contents":2}]}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":1}]}]}],null],["function/computation( lambda (x.apply_x))",[["A","B","f1","f2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}],null]],[]]},{"tag":"Paragraph","contents":"*Note*: The function computation rule is defined the way it is due to a current limitations in Holbert's unifier. The intermediate $b:b$ variable and $b f2 a2: _=_ b (f2 a2)$ premise should not be necessary. For more information see the following toot: ~https://types.pl/@liamoc/108286374881642482~"},{"tag":"Heading","contents":[2,"Non-dependent Function Types"]},{"tag":"Paragraph","contents":"Non-dependent function types use arrow notation $A B:_->_ A B$, which we define in terms of dependent function types:"},{"tag":"Rule","contents":["Axiom",[["eq/arrow-type",[["A","B"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":1}]}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Statics"]},{"tag":"Paragraph","contents":"The formation rule for non-dependent function types follows from dependent function types:"},{"tag":"Rule","contents":["Theorem",[["arrow/formation",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],[[null,["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":1}]}]}]},[{"tag":"Defn","contents":"function/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":0},[]]],[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]]]]]]]],10]]],[]]},{"tag":"Paragraph","contents":"The same goes for the introduction and elimination rules:"},{"tag":"Rule","contents":["Theorem",[["arrow/introduction",[["A","B","b"],[[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]}],[[null,["A","B","b"],[[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":2}]}]}]},[{"tag":"Defn","contents":"function/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]},[{"tag":"Local","contents":0},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]},[{"tag":"Local","contents":1},[]]]]]]]]]]]],16]]],[]]},{"tag":"Rule","contents":["Theorem",[["arrow/elimination",[["A","B","f","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]}],[[{"subtitle":"Show:","proseStyle":false},["A","B","f","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]},[{"tag":"Defn","contents":"function/elimination"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":3}]}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},true]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Local","contents":0},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]},[{"tag":"Local","contents":1},[]]]]]],62]]],[]]},{"tag":"Heading","contents":[3,"Dynamics"]},{"tag":"Paragraph","contents":"Todo: derive computation rules"},{"tag":"Heading","contents":[2,"Dependent Pair Types"]},{"tag":"Paragraph","contents":"Dependent pair types are pair types where the type of the second element of the pair might depend on the first element of the pair. These are also known as ‘dependent sum types’, which is where the $Sigma$ notation comes from."},{"tag":"Heading","contents":[3,"Statics"]},{"tag":"Rule","contents":["Axiom",[["pair/formation",[["A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":1}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["pair/introduction",[["A","B","a","b"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":3}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["pair/elimination(proj1_)",[["A","B","p"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":2}]}],null],["pair/elimination(proj2_)",[["A","B","p"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj2"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":0}]}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Dynamics"]},{"tag":"Rule","contents":["Axiom",[["pair/equal( Sigma__)",[["A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["pair/equal(_,_)",[["A","B","a1","a2","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":5}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":4},{"tag":"LocalVar","contents":3}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":5}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]}]}],null],["pair/equal(proj1_)",[["A","B","p1","p2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":3}]}],null],["pair/equal(proj2_)",[["A","B","p1","p2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj2"},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj2"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":1}]}]}]}],null],["pair/computation(proj1 (_,_))",[["A","B","a1","a2","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":5}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":6}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]}]},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":5}]}],null],["pair/computation(proj2 (_,_))",[["A","B","a1","a2","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":5}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":6}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":0}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj2"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":4},{"tag":"LocalVar","contents":3}]}]}],null],["pair/computation((proj1 _,proj2 _))",[["A","B","p1","p2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_,_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj1"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"proj2"},{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]}]}]}]}],null]],[]]},{"tag":"Heading","contents":[2,"Non-dependent Pair Types"]},{"tag":"Rule","contents":["Axiom",[["product/formation",[["A","B"],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_times_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":1}]}]}]}],null]],[]]},{"tag":"Paragraph","contents":"Todo"},{"tag":"Heading","contents":[2,"Enumeration Sets"]},{"tag":"Paragraph","contents":"Todo"},{"tag":"Heading","contents":[2,"Equality Types"]},{"tag":"Paragraph","contents":"Todo: description"},{"tag":"Heading","contents":[3,"Statics"]},{"tag":"Rule","contents":["Axiom",[["equality/formation",[["n","A","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":2}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":2}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],null],["equality/introduction",[["A","a1","a2","a3"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":3}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":3}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":3}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"LocalVar","contents":2}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],null],["equality/elimination",[["A","a1","a2","eq-a","B","b"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":5}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"Const","contents":":"}]},{"tag":"LocalVar","contents":5}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"Const","contents":":"}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":3}]}]}],[["x1","x2","eq-x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":8}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":8}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":8}]},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":4},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":6}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"LocalVar","contents":0}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"eq-ind"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Dynamics"]},{"tag":"Rule","contents":["Axiom",[["equality/equal(Eq___)",[["A","B","a1","a2","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":4}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":5}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":5}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],null],["equality/equal(refl_)",[["A","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]}]}],null],["equality/equal(eq-ind__)",[["A","a1","a2","a3","a4","eq-a1","eq-a2","B","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":8}]},{"tag":"LocalVar","contents":6}]},{"tag":"LocalVar","contents":9}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":7}]},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":9}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":3}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":9}]},{"tag":"LocalVar","contents":8}]},{"tag":"LocalVar","contents":7}]}]}],[["x1","x2","eq-x"],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":5},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":10}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":3},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"LocalVar","contents":0}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"eq-ind"},{"tag":"LocalVar","contents":4}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"eq-ind"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":8}]},{"tag":"LocalVar","contents":7}]},{"tag":"LocalVar","contents":4}]}]}],null],["equality/computation(eq-ind(refl_)_)",[[],[[[],[],{"tag":"Const","contents":"???"}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"eq-ind"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"refl"},{"tag":"Const","contents":"_"}]},{"tag":"Const","contents":"_"}]}]},{"tag":"Const","contents":"_"}]}]},{"tag":"Const","contents":"???"}]},{"tag":"Const","contents":"???"}]}],null]],[]]},{"tag":"Paragraph","contents":"Todo:\n\n- rewrite\n- congruence\n- reflexivity\n- symmetry"},{"tag":"Heading","contents":[2,"Levels"]},{"tag":"Paragraph","contents":"We are about to define universes, which are types that serve as descriptions of other types. Since universes are also types, it might seem reasonable to let universes describe other universes. Alas, this runs the risk of introducing self-referential paradoxes like the ones found by Russell, Girard, and Hurkens. To avoid these issues we first define /universe levels/ in the form of natural numbers. These will be used to mark the ‘size’ of universes, ensuring that smaller universes can only ever inhabit larger universes."},{"tag":"Rule","contents":["Axiom",[["level/formation",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Const","contents":"Lvl"}]}],null],["level/introduction(0)",[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]}],null],["level/introduction(s_)",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"Lvl"}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Const","contents":"Lvl"}]}],null]],[]]},{"tag":"Heading","contents":[2,"Universes"]},{"tag":"Paragraph","contents":"Now that we have defined our levels, we are now ready to define the type of universes. We take a Russell-style approach, where types inhabit universes directly."},{"tag":"Paragraph","contents":"*Note*: We do not provide introduction rules for $Lvl$, as this would result in further inconsistencies to our type theory. If we wanted to support level polymorphism we would probably have to pursue something like Agda’s $Setω$. ~https://agda.readthedocs.io/en/latest/language/sort-system.html#sorts-seti~."},{"tag":"Heading","contents":[3,"Statics"]},{"tag":"Rule","contents":["Axiom",[["universe/formation",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"Lvl"}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":0}]}]}],null],["universe/introduction(U_)",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"Lvl"}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"LocalVar","contents":0}]}]}]}],null],["universe/introduction( Pi__)",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":3}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],null],["universe/introduction( Sigma__)",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":3}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],null],["universe/introduction(Eq__)",[["n","A","a1","a2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":3}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":2}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":3}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Dynamics"]},{"tag":"Rule","contents":["Axiom",[["universe/equal(U_)",[["n"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Const","contents":"Lvl"}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":0}]}]}],null],["universe/equal( Pi__)",[["n","A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":5}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],null],["universe/equal( Sigma__)",[["n","A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],[["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":5}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":2},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Sigma"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"LocalVar","contents":1},{"tag":"LocalVar","contents":0}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],null],["universe/equal(Eq__)",[["n","A","B","a1","a2","b1","b2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":4}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":6}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":5}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":5}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":5}]},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Eq"},{"tag":"LocalVar","contents":4}]},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":6}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Cumulativity"]},{"tag":"Paragraph","contents":"Types inhabiting smaller universes also inhabit larger universes by way of the inclusion rule. This gives us a cumulative hierarchy of universes where $n m: U n <= U m$."},{"tag":"Rule","contents":["Axiom",[["universe/inclusion",[["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"LocalVar","contents":1}]}]}]}],null]],[]]},{"tag":"Heading","contents":[3,"Forming Types From Universes"]},{"tag":"Paragraph","contents":"We can form a type $A:A$ if it is an element of $l:U l$."},{"tag":"Rule","contents":["Axiom",[["type/formation",[["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Const","contents":"Lvl"}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]}],null]],[]]},{"tag":"Paragraph","contents":"Likewise we can say that two types $A:A$ and $B:B$ are equal types if the are also equal elements of $n:U n$."},{"tag":"Rule","contents":["Axiom",[["type/equal",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"Const","contents":"Lvl"}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}],null]],[]]},{"tag":"Heading","contents":[3,"Derived Universe Rules"]},{"tag":"Rule","contents":["Theorem",[["universe/introduction(_->_)",[["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],[[null,["n","A","B"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":1}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Defn","contents":"universe/introduction( Pi__)"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Local","contents":0},[]]],[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":3}]}]},[{"tag":"Local","contents":1},[]]]]]]]]],9]]],[]]},{"tag":"Rule","contents":["Theorem",[["universe/equal( _->_ )",[["n","A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],[[null,["n","A1","A2","B1","B2"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":2}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},false]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":3}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":2}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":2}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":1}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]},[{"tag":"Defn","contents":"universe/equal( Pi__)"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":3}]},{"tag":"LocalVar","contents":2}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":4}]}]},[{"tag":"Local","contents":0},[]]],[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":4}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":2}]},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":5}]}]},[{"tag":"Local","contents":1},[]]]]]]]]]]]],25]]],[]]},{"tag":"Heading","contents":[2,"Examples"]},{"tag":"Paragraph","contents":"This section shows some examples of some proofs using the above rules."},{"tag":"Rule","contents":["Theorem",[["example/form-hom",[[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}]}]}],[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"function/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"universe/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Defn","contents":"level/introduction(0)"},[]]]]]],[null,["A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"arrow/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]},[{"tag":"Defn","contents":"type/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Defn","contents":"level/introduction(0)"},[]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":0},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"LocalVar","contents":0}]},[{"tag":"Defn","contents":"type/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Defn","contents":"level/introduction(0)"},[]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":0},[]]]]]]]]]]]],34]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/intro-id-simple",[["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}],[[null,["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"arrow/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]]]]],3]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/compute-apply-id-simple",[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]}],[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Defn","contents":"function/computation(apply( lambda_)_)"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Local","contents":0},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Ap","contents":[{"tag":"Const","contents":"s"},{"tag":"Const","contents":"0"}]}]}]},[{"tag":"Defn","contents":"universe/introduction(U_)"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Defn","contents":"level/introduction(0)"},[]]]]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Refl"},[]]]]]],13]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/intro-id",[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}]}]}],[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}]}]},[{"tag":"Defn","contents":"function/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"arrow/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]]]]]]]],6]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/compute-apply-id",[["Thing"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]}],[[null,["Thing"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"function/computation(apply( lambda_)_)"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"arrow/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]},[{"tag":"Local","contents":2},[]]]]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":0},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},[{"tag":"Refl"},[]]]]]],15]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/compute-apply-apply-id",[["Thing","thing"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}],[[{"subtitle":"Show:","proseStyle":true},["Thing","thing"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Defn","contents":"equal-term/trans"},[[{"subtitle":"Show:","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Defn","contents":"function/equal(apply__)"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"LocalVar","contents":1}]},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":2}]}]}]},[{"tag":"Rewrite","contents":[{"tag":"Defn","contents":"eq/arrow-type"},true]},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["A",{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"example/compute-apply-id"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":0},[]]]]]]]]],[{"subtitle":"Show:","proseStyle":false},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]]]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Defn","contents":"function/computation(apply( lambda_)_)"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":2}]},[{"tag":"Local","contents":2},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},[{"tag":"Refl"},[]]]]]]]]],123]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/elim-apply-id-type",[["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}],[[null,["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"arrow/elimination"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_->_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]},[{"tag":"Defn","contents":"arrow/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Local","contents":1},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Local","contents":0},[]]]]]],7]]],[]]},{"tag":"Rule","contents":["Theorem",[["example/form-apply-id",[["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Const","contents":"Lvl"}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]}],[[null,["n","A"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Const","contents":"Lvl"}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]}]],{"tag":"Ap","contents":[{"tag":"Const","contents":"_type"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},[{"tag":"Defn","contents":"type/formation"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Local","contents":0},[]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":0}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"function/elimination"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"Pi"},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},{"tag":"Lam","contents":["x",{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]}]},[{"tag":"Defn","contents":"function/introduction"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":2}]}]},[{"tag":"Local","contents":2},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Local","contents":1},[]]]]]]]]],9]]],[]]},{"tag":"Paragraph","contents":"We should be able to compute in type annotations:"},{"tag":"Rule","contents":["Theorem",[["example/apply-id-ann",[["A","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":1}]}]}],[[{"subtitle":"Show:","proseStyle":false},["A","a"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}],[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"term/equal-type"},[[{"subtitle":"Show:","proseStyle":true},[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Local","contents":1},[]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_type"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":1}]}]},[{"tag":"Defn","contents":"type/equal"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"Const","contents":"0"}]},{"tag":"Const","contents":"Lvl"}]},[{"tag":"Defn","contents":"level/introduction(0)"},[]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"equal-term/symm"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"apply"},{"tag":"Ap","contents":[{"tag":"Const","contents":"lambda"},{"tag":"Lam","contents":["x",{"tag":"LocalVar","contents":0}]}]}]},{"tag":"LocalVar","contents":1}]}]},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"function/computation(apply( lambda_)_)"},[[null,["x"],[[[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]}]],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":0}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":2},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_==_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Defn","contents":"equal-term/refl"},[[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_:_"},{"tag":"LocalVar","contents":1}]},{"tag":"Ap","contents":[{"tag":"Const","contents":"U"},{"tag":"Const","contents":"0"}]}]},[{"tag":"Local","contents":0},[]]]]]],[null,[],[],{"tag":"Ap","contents":[{"tag":"Ap","contents":[{"tag":"Const","contents":"_=_"},{"tag":"LocalVar","contents":1}]},{"tag":"LocalVar","contents":1}]},[{"tag":"Refl"},[]]]]]]]]]]]]]]],172]]],[]]}] |
