l (a : IW I A B i j l) : forall b, Decidable (a = b). Proof. destruct a as [x c1]. intro b. transparent assert (decide_children : (forall c2, Decidable (c1 = c2))). { intros c2. destruct (liftP x (fun c => c1 c = c2 c) (fun c => _ (c1 c) (c2 c))) as [p|p]. + left; by apply path_forall. + right; intro h; by apply p, apD10. } snrefine ( match b in (IW _ _ _ _ _ l) return forall iy : l = i x, Decidable (iw_sup I A B i j x c1 = paths_rec l (IW I A B i j) b (i x) iy) with iw_sup y c2 => fun iy : i y = i x => _ end idpath). destruct (fibers_dec (i x) (x ; idpath) (y ; iy)) as [feq|fneq]. + refine ( match feq in (_ = (y ; iy)) return forall c2, Decidable (iw_sup _ _ _ _ _ x c1 = paths_rec (i y) (IW I A B i j) (iw_sup _ _ _ _ _ y c2) (i x) iy) with idpath => _ end c2). cbn; intros c3. destruct (decide_children c3) as [ceq | cneq]. - left; exact (ap _ ceq). - right; intros r; apply cneq. exact (children_eq x c1 c3 r). + right; intros r; apply fneq. exact (ap getfib r @ getfib_computes x y c2 iy). Defined.
Require Import Basics. Require Import Types.Forall Types.Sigma Types.Prod Types.WType.