equiv_functor_arrow' `(f : B <~> A) `(g : C <~> D) : (A -> C) <~> (B -> D) := @equiv_functor_forall' _ A (fun _ => C) B (fun _ => D) f (fun _ => g). End AssumeFunext. Global Instance decidable_arrow {A B : Type} `{Decidable A} `{Decidable B} : Decidable (A -> B). Proof. destruct (dec B) as [x2|y2]. - exact (inl (fun _ => x2)). - destruct (dec A) as [x1|y1]. + apply inr; intros f. exact (y2 (f x1)). + apply inl; intros x1. elim (y1 x1). Defined.
Require Import Basics.Overture Basics.PathGroupoids Basics.Decidable Require Import Types.Forall.