proposition: Lemma retr : forall (Δ : Tel) (u v : Δ), Sect (eq_eq_equiv Δ u v) (eq_eq_equiv_inv Δ u v).
proof: Proof. induction Δ. + simpl. intros. intro. constructor. + intros u v e. simpl. specialize (H v.1 (rew (equiv_inv (IsEquiv := path_sigma_equiv _ _ _) e).1 in u.2) v.2 (equiv_inv (IsEquiv := path_sigma_equiv _ _ _) e).2). set (foo := eq_eq_equiv_inv _ _ _ _) in *. symmetry in H. clearbody foo. revert foo H. refine (Top.subst2 _). refine (eisretr (path_sigma_uncurried u v) _). Defined.
imports: Equations DepElimDec EqDecInstances