[Agda] Help at propositional equality proof that contains subst.

[Martin Escardo]

On 04/05/17 06:44, apostolis.xekoukoulotakis at gmail.com wrote:
> This seems to be closer to what my code actually looks like:
>
> postulate
>   B : Set
>   A : B → Set
>   big_expression : (c : B) → {b : B} → (a : A b) → B
>   h : (c : B) → {b : B} → (a : A b) → A (big_expression c a)
>   eq : (c : B) → {b : B} → (a : A b) → (big_expression c a) ≡ c
>
> f : {b : B} → (a : A b) → subst A (eq b a) (h b a) ≡ a
> f = {!!}

We have

   eq b a : big_expression b a = b
   h b a  : A(big_expression b a)

Consider the instantiations

   A b = Bool
   big_expression c {b} a = c
   h c {b} a = true
   eq b a = refl

So the type subst A (eq b a) (h b a) ≡ a amounts to

             subst A refl true = a,

that is,
             true = a.

Hence we have

   f : {b : B} → (a : Bool) → true ≡ a

which of course can't be proved.

Hence, in the generality you have things above, you can't complete the
definition of f.

Of course it may well be that for your specific B, A, big_expression,
h and eq, you can complete the definition of f.

You will need to cook-up a more specific abstraction of your code
for us to be able to help more here in this list.

I hope this helps.

Martin