proposition: Lemma equiv_cong_subst_tel_dep {Δ : Tel} (Γ : Δ -> Tel) (f : forall x : Δ, Γ x) (P : forall (x : Δ), Γ x -> Type) (s t : Δ) (e : s =={Δ} t) (u : P _ (f s)) (v : P t (f t)) : u ==_{(fun x => P x (f x)); e} v <~> (J _ (fun y e => P y (subst _ e (f s))) (transport_u Γ f P s u) _ e ==_{(fun x => P _ x); dcong_tel f e} v).
proof: Proof. unfold subst. revert t e v. refine (J _ _ _). intros. rewrite J_refl. unfold transport_u. unfold eq_rect_r. simpl. Admitted. Definition lifted_solution_rhs_type (Γ : Tel) (u v : Γ) (Γ' : Tel) (Δ : Γ -> Tel) (a b : forall ρ, Δ ρ) (eqΔ := λ ρ, a ρ =={Δ ρ} b ρ) (r : a u =={Δ u} b u) (s : a v =={Δ v} b v) (f : extend_tele Γ (fun ρ => eq (Δ ρ) (a ρ) (b ρ)) <~> Γ') := f (inj_extend_tel Γ eqΔ u r) =={Γ'} f (inj_extend_tel Γ eqΔ v s). Definition lifted_solution (Γ : Tel) (u v : Γ) (Γ' : Tel) (Δ : Γ -> Tel) (a b : forall ρ, Δ ρ) (eqΔ := λ ρ, a ρ =={Δ ρ} b ρ) (r : eqΔ u) (s : eqΔ v) (f : extend_tele Γ eqΔ <~> Γ') : lifted_solution_lhs_type Γ u v Δ a b r s <~> lifted_solution_rhs_type Γ u v Γ' Δ a b r s f. Proof. unfold lifted_solution_rhs_type. unfold lifted_solution_lhs_type. refine (equiv_compose _ _). unshelve refine (@equiv_tele_r _ _ _ _). intros x. set(lhs:=dcong_tel a x). set(rhs:=dcong_tel b x). unfold eqΔ in r, s. exact (@square _ _ _ _ _ (inv_equiv (eq_points_equiv _ _ _) lhs) (inv_equiv (eq_points_equiv _ _ _) rhs) (cong _ _ _ r) (inv_equiv (eq_points_equiv (Δ v) (a v) (b v)) s) ). simpl. intros x. apply flip_square_equiv. pose (cong_equiv (extend_tele Γ eqΔ) (inj_extend_tel Γ eqΔ u r) (inj_extend_tel Γ eqΔ v s) _ f _). refine (equiv_compose _ _). Focus 2. refine (eq_points_equiv _ _ _). refine (equiv_compose _ _). Focus 2. refine e. refine (equiv_compose _ _). refine (equiv_sym _). cbv beta zeta. refine (reorder_tele (u =={Γ} v) (fun x => inj (square (inv_equiv (eq_points_equiv (Δ v) (subst (λ x0 : Γ, Δ x0) x (a u)) (a v)) (dcong_tel a x)) (inv_equiv (eq_points_equiv (Δ v) (subst (λ x0 : Γ, Δ x0) x (b u)) (b v)) (dcong_tel b x)) (cong (subst (λ x0 : Γ, Δ x0) x) (a u) (b u) r) (inv_equiv (eq_points_equiv (Δ v) (a v) (b v)) s)))). clear. unfold eqΔ. simpl. induction Γ. - simpl extend_tele. simpl inj_extend_tel. refine (equiv_tele_r _). intros x. revert v x s. refine (Top.J _ _). intros s. simpl. unfold square. unfold dcong_tel. simpl. unfold Telescopes.dcong_tel_obligation_1. simpl. subst eqΔ. simpl in *. unfold subst. simpl. unfold eq_over_refl. simpl. unfold eq_rect_r. simpl. set (au := a u) in *. set (bu := b u) in *. unfold dcong_tel. simpl. clearbody bu. clearbody au. revert bu r s. refine (J _ _ _). intros s. unfold cong. rewrite J_refl. unfold inv_equiv, eq_points_equiv. unfold equiv_inv. simpl. rewrite eq_eq_equiv_inv_refl. simpl. unshelve refine {| equiv a := _ |}. apply (Top.cong (equiv (eq_points_equiv (Δ u) au au))) in a. unfold equiv in a. simpl in a. unfold inv_equiv in a. simpl in a. rewrite eq_eq_equiv_refl in a. symmetry in a. destruct a. pose proof (eisretr (eq_eq_equiv (Δ u) au au)). red in H. specialize (H s). rewrite H. apply refl. unshelve refine {| equiv_inv a := _ |}. revert s a. refine (J _ _ _). symmetry. apply eq_eq_equiv_inv_refl. + red. intros. revert s x. refine (J _ _ _). simpl. unfold eq_sym, Logic.eq_ind. simpl. apply axiom. + apply axiom. + apply axiom. - apply axiom. Defined.
imports: Equations DepElimDec EqDecInstances Utf8