proposition: Lemma inj_extend_tel_tele (Γ : Tel) (Δ : Γ -> Tel) u v a b (f := fun ρ => a ρ =={Δ ρ} b ρ) (r : f u) (s : f v) : inj_extend_tel Γ f u r =={extend_tele Γ f} inj_extend_tel Γ f v s <~> tele (x : u =={Γ} v) in (subst (fun y => telescope (b u =={Δ;x} y)) s (subst (fun y => telescope (y =={Δ;x} a v)) r (dcong_tel a x)) =={b u =={Δ;x} b v} dcong_tel b x).
proof: Proof. Admitted. 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_tel_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_tel_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_tel _ _ _ _ _ (cong_tel _ _ _ r) s lhs rhs ). intros x. simpl. unfold theorem_square. apply flip_square_tel_equiv. refine (equiv_compose _ _). Focus 2. refine (eq_points_equiv _ _ _). refine (equiv_compose _ _). Focus 2. refine (cong_equiv (extend_tele Γ eqΔ) (inj_extend_tel Γ eqΔ u r) (inj_extend_tel Γ eqΔ v s) _ f _). refine (equiv_compose _ _). refine (equiv_tele_r _). intro. refine (equiv_compose _ _). simpl. unfold square_tel. unfold eqΔ in r, s. set (lhs := dcong_tel a x). set (rhs := dcong_tel b x). pose (@equiv_cong_subst_tel (Δ u) (Δ v) (fun x => x == a v) (subst Δ x) (a u) (b u) r lhs). simpl in e. specialize (e (subst (λ x0 : Δ u, subst (λ x : Γ, Δ x) x x0 == a v) r lhs)). rewrite e. refine (equiv_id _). refine (equiv_id _). refine (equiv_compose _ _). refine (equiv_sym _). cbv beta zeta. refine (reorder_tele (u =={Γ} v) (fun x => _)). clear f. induction Γ. Transparent telescope eq. - 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_tel. unfold dcong_tel. simpl. unfold Telescopes.dcong_tel_obligation_1. simpl. unfold eq_rect_r. simpl. subst eqΔ. simpl in *. unfold subst. simpl. set (au := a u) in *. set (bu := b u) in *. clearbody bu. clearbody au. revert bu r s. refine (J _ _ _). intros s. rewrite J_refl. apply axiom. - simpl. refine (equiv_tele_r _). intros. destruct v. simpl in *. subst eqΔ. simpl in *. revert pr1 x pr2 s. refine (Top.J _ _). simpl. intros. specialize (X u.1 u.2 pr2). specialize (X (fun ρ => Δ &(u.1 & ρ))). simpl in X. specialize (X (fun ρ => a &(u.1 & ρ)) (fun ρ => b &(u.1 & ρ))). simpl in X. destruct u. simpl in *. specialize (X r s). apply X. Defined.
imports: Equations DepElimDec EqDecInstances Utf8