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.