coq - Cong, subst and equality type in dependently typed programming languages -


in dependently typed type theory there's equality type. when type defined, number of utilities, namely cong , subst introduced. how expressive are? possible express can eliminator equality them?

no, can't prove uniqueness of identity proofs cong, subst , eliminator.

uip : {α : level} {a : set α} {x y : a} -> (p q : x ≡ y) -> p ≡ q

here explanation: http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/


Comments

Post a Comment

Popular posts from this blog

user interface - How to replace the Python logo in a Tkinter-based Python GUI app? -

is there way change default logo, python logo , appears in window's task bar? notice have replaced default tk logo used appear in application window. i using windows 7 , python 2.6 , developing gui of tkinter. you can using winico tk extension package. winico package can used add system tray icons tk programs. the following sample shows 1 way change runtime application icon. note need provide .ico file suitable sizes of icons in on command line , need use pythonw. not change taskbar icon console when running python script. test extracted winico0.6 package python\tcl\winico0.6 folder package require winico work , ran code below using pythonw winico_test.py path\to\some\ico\file.ico . import sys tkinter import * def main(argv): root = tk() root.update() root.tk.call('package','require','winico') id = root.tk.call('winico','createfrom',argv[1]) root.tk.call('winico','setwindow',root,id...
Read more

android - Get AccessToken using signpost OAuth without opening a browser (Two legged Oauth) -

i using signpost oauth access data magento server. have read various tutorials on same , reach point open browser user can enter credentials. however, per requirement have automate part. hence, user should not browser page. have set-up done on server side ( magento ), hit url , returned call page. same through program in android. i have tried below, consumer = new commonshttpoauthconsumer(key, secret); provider = new commonshttpoauthprovider(oauth_init_url,access_token_url, authorize_url); try { provider.retrieverequesttoken(consumer, oauth.out_of_band); log.d("tokens" , consumer.gettoken() + " -- " + consumer.gettokensecret()); } and request tokens. dont know how bypass next step. tried directly accessing accesstoken (stupid of me) provider.retrieveaccesstoken(consumer, "mycallback://callback"); no luck, ends in oauth.signpost.exception.oauthnotauthorizedexception: authorization failed (server replied 401). ...
Read more

org.mockito.exceptions.misusing.InvalidUseOfMatchersException: mockito -

getting error org.mockito.exceptions.misusing.invaliduseofmatchersexception: invalid use of argument matchers! 1 matchers expected, 2 recorded. exception may occur if matchers combined raw values: //incorrect: somemethod(anyobject(), "raw string"); when using matchers, arguments have provided matchers. example: //correct: somemethod(anyobject(), eq("string matcher")); at when( getprogramservice .callservice(any(getprogramtype.class))) .thenreturn(jaxbresponse); please explain error , possible resolution the code posted looks fine; don't see problem it. code before or above causing exception. key here: invalid use of argument matchers! 1 matchers expected, 2 recorded. any , used above, doesn't return "special kind of null" or "special kind of getprogramtype"; don't exist. instead, returns null , side effect puts matcher on stack. whe...
Read more