[Agda] How to case split on the value of a function (the second
time)?
Jacques Carette
carette at mcmaster.ca
Mon Dec 9 04:25:15 CET 2013
On 2013-12-08 17:22 , Nils Anders Danielsson wrote:
> On 2013-12-06 17:40, Jacques Carette wrote:
>> sub1 : {A B : Set} → ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A → B
>> sub1congr : {A B : Set} → (eq : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) → {x : A} →
>> (((sub1 eq) ○ (sub1 (sym≃ eq))) x ≡ x)
>
> I've proved a similar property about a similar function, see
> Fin.⊎-left-cancellative:
>
> http://www.cse.chalmers.se/~nad/listings/equality/Function-universe.html#41160
That is indeed a very similar function, thanks. I did manage to prove
mine, using ideas [in hindsight] very similar to those you used. Your
proof is certainly visually much more appealing than mine -- this
encourages me to keep optimizing my proof.
Jacques
More information about the Agda
mailing list