Still trying to get my brain around functions.v, there's a typical situation I don't see how to handle: an induced function.

Here is a small sample code to discuss the issue at hand:

```
From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp classical_sets.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Open Scope classical_set_scope.
Section InitialProblem.
Variable X Y Z: Type.
Variable A: set X.
Variable f: A -> Y.
Variable B: set Y.
Variable g: B -> Y.
Hypothesis composable: forall a, f a \in B.
Variable a: A.
Check f a.
Fail Check (g \o f) a. (* as expected *)
(* FIXME: how to turn the fact `f a \in B` into some kind of typing judgement `f a: B`?
=> the question doesn't make sense as-is, but the situation is pretty usual in mathematics
*)
End InitialProblem.
Section MinimalProblem.
Variable Y: Type.
Variable B: set Y.
Variable b: Y.
Hypothesis bB: b \in B.
(* FIXME: better question: from this data, how to build a `whatever b bB` of type B ? *)
(* `val` is essentially the reverse, if I get it right *)
End MinimalProblem.
```

Last updated: Jun 22 2024 at 15:01 UTC