Talk:Proof: Difference between revisions
→Quantifiers
Line 229:
::: By "you" you mean anybody who "believe" in Agda/Coq/Epigram/Twelf/ATS/NuPRL/ALF/DML/LEGO/HOL/Isabele/ACL2/Mizar/MetaMath/etc. proofs? Did you believe in 4-color theorem proof? Did you reject implementations of the homotopy type theory in Coq/Agda?
:::: If your description here is correct, then these implementations of homotopy type theory have weaknesses in their treatment of upper bounds. No big deal, perhaps, except that you seem rather intolerant of other implementations with the same kind of limitation. --[[User:Rdm|Rdm]] 01:53, 14 May 2012 (UTC)
::: My current inclination is to believe that you cannot get [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf the point] of dependently-typed programming languages / proof systems. — [[User:Ht|Ht]] 23:00, 13 May 2012 (UTC)
| |||