proposition: Lemma functor_ext : forall (C D : ord_category) (F G : ord_functor C D), (forall A : C, F A = G A) -> F = G.
proof: Proof. intros C D F G H. apply boolp.funext in H. destruct F as [F F2 F3 F4 F5]. destruct G as [G G2 G3 G4 G5]. simpl in H. move: F2 F3 F4 F5 G2 G3 G4 G5. rewrite !H. intuition. assert (FG2 : F2 = G2). Abort. End Extensionality_for_ordfunctors. Section RelativeFreeMonad. Context (S : Type) (P : S -> choiceType). Inductive rFreeF (A : choiceType) : Type := | retrFree : A -> rFreeF A | ropr : forall s, (P s -> rFreeF A) -> rFreeF A. Arguments ropr [A] _ _. Fixpoint bindrFree {A B : choiceType} (c : rFreeF A) (k : TypeCat ⦅ choice_incl A ; rFreeF B ⦆ ) : rFreeF B := match c with | retrFree a => k a | ropr s ar => ropr s (fun p => bindrFree (ar p) k) end. Definition callrFree (s : S) : rFreeF (P s) := ropr s (fun k => retrFree _ k). Program Definition rFree : ord_relativeMonad choice_incl := @mkOrdRelativeMonad ord_choiceType TypeCat choice_incl rFreeF _ _ _ _ _ _. Next Obligation. constructor. assumption. Defined.
imports: mathcomp(all_ssreflect boolp) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd choice_type) Crypt(SubDistr)