[Agda] How to case split on the value of a function (the second time)?

[Andreas Abel]

Hi Jacques,

Could you provide an Agda file (or a tgz/zip if it are several) or a 
clone instruction for your repo?  It is just so much easier to answer if 
there is some Agda code to play with.

Cheers,
Andreas

On 06.12.2013 17:40, Jacques Carette wrote:
> So I have a function
> sub1 : {A B : Set} → ((⊤ ⊎ A) ≃ (⊤ ⊎ B)) → A → B
> which given an isomorphism as above, will extract a function A → B. Now,
> that function actually has some nice properties, which I would like to
> prove, such as
>
> sub1congr : {A B : Set} → (eq : (⊤ ⊎ A) ≃ (⊤ ⊎ B)) → {x : A} → (((sub1
> eq) ○ (sub1 (sym≃ eq))) x ≡ x)
>
> where sym≃ is symmetry of isomorphism. The "problem" is that sub1 is
> written as a case split on the values of the underlying isomorphism
> (i.e. eq contains a function f : (⊤ ⊎ A) → (⊤ ⊎ B) and I do a case-split
> on the range). This works for getting sub1 defined. I do need to make
> use of the 'inspect' idiom in there.
>
> However, no matter what I do, I cannot get the goals in sub1congr to
> reduce given the same case split.
>
> Any advice?
>
> Jacques
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>