Encoding Structural Equality in CaPriCon 'utils require import Try It Out > Required module: utils Type 'A -> A 'x -> 'Eq_context { A 'a -> Type ? '.Eq -> .Eq ( x ) '.refl -> } def 'Eq A 'y -> Eq_context .Eq ( y ) ? ? "x = y" defconstr ! 'refl Eq_context .refl ! ! "refl x" defconstr Try It Out > The type of \(λ(\mathrm{y}:\mathrm{A})\,(\mathrm{e}:\mathrm{x}\,=\,\mathrm{y}).\,\mu(\mathrm{e})\) A ’y -> Eq ( y ) ’e recursor dup ! tex is \(∀(\mathrm{y}:\mathrm{A})\,(\mathrm{e}:\mathrm{x}\,=\,\mathrm{y})\,(\mathrm{Eq}^P:∀(\mathrm{a}:\mathrm{A}),\,\mathrm{x}\,=\,\mathrm{a} \rightarrow Set_{1}),\,\mathrm{Eq}^P\,\mathrm{x}\,(refl\,\mathrm{x}) \rightarrow \mathrm{Eq}^P\,\mathrm{y}\,\mathrm{e}\) type tex. 2 lambdas [ 'Eq 'refl ] { export } each Try It Out >