projects / ~helmut / bidiragda.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 69f47ca) | patch
turns out: ind-cong is a special case of H.cong₂
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 5 Jan 2015 09:40:23 +0000 (10:40 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 5 Jan 2015 09:40:23 +0000 (10:40 +0100)
commitc5f982320394b5083e4ebca921c1cd5e88df9b14
treeb397cf1fb4ee697699fe59031c3203c68e46266btree | snapshot
parent69f47cad0ac14a7549e1e94b9f9a40f9935ad99ecommit | diff
turns out: ind-cong is a special case of H.cong₂

The major differences between them are:
 * ind-cong treats the first parameter to the function implicit whereas
   H.cong₂ makes it explicit.
 * ind-cong expects a propositional proof for the first equality whereas
   H.cong₂ asks for a heterogeneous one. Lift using H.reflexive.
LiftGet.agda diff | blob | history
Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)