proposition: Lemma Z_abs_respects' : forall (x y : PairT.T N) (E : PairT.equiv x y), transport (fun q : Z => (exists n : N, naturals_to_semiring N Z n = q) |_| (exists n : N, naturals_to_semiring N Z n = - q)) (Z_path E) (Z_abs_def x) = Z_abs_def y.
proof: Proof. intros [pa pb] [na nb] E. red in E; simpl in E. unfold Z_abs_def. destruct (nat_distance_sig pa pb) as [[z1 E1] | [z1 E1]];simpl. - destruct (dec (z1 = 0)) as [E2 | E2]. + rewrite Sum.transport_sum. rewrite Sigma.transport_sigma. destruct (nat_distance_sig na nb) as [[z2 E3] | [z2 E3]]; [destruct (dec (z2 = 0)) as [E4 | E4]|];simpl. * apply ap. apply Sigma.path_sigma_hprop;simpl. apply PathGroupoids.transport_const. * destruct E4. rewrite <-E1,<-E3,E2,plus_0_r,<-(plus_0_r (na+pa)) in E. rewrite plus_assoc,(plus_comm pa) in E. apply (left_cancellation plus _) in E. trivial. * apply ap. apply Sigma.path_sigma_hprop. simpl. rewrite PathGroupoids.transport_const. rewrite E2,plus_0_r in E1. rewrite <-E3,E1 in E. apply (left_cancellation plus (pb + nb)). rewrite plus_0_r. etransitivity;[apply E|]. ring_with_nat. + rewrite Sum.transport_sum,Sigma.transport_sigma. destruct (nat_distance_sig na nb) as [[z2 E3] | [z2 E3]]; [destruct (dec (z2 = 0)) as [E4 | E4]|];simpl. * destruct E2. rewrite E4,plus_0_r in E3;rewrite <-E1,<-E3 in E. apply (left_cancellation plus (pa+na)). rewrite (plus_comm pa na),plus_0_r,<-plus_assoc. rewrite (plus_comm na pa). symmetry;trivial. * apply ap. apply Sigma.path_sigma_hprop. simpl. rewrite PathGroupoids.transport_const. rewrite <-E1,<-E3 in E. apply (left_cancellation plus (pa + na)). rewrite <-(plus_assoc pa na z2),(plus_comm pa na),<-plus_assoc. symmetry;trivial. * destruct E2. rewrite <-E1,<-E3 in E. assert (Erw : nb + z2 + (pa + z1) = (pa + nb) + (z2 + z1)) by ring_with_nat. rewrite <-(plus_0_r (pa+nb)),Erw in E. apply (left_cancellation plus _),symmetry,naturals.zero_sum in E. apply E. - rewrite Sum.transport_sum,Sigma.transport_sigma. simpl. destruct (nat_distance_sig na nb) as [[z2 E3] | [z2 E3]]; [destruct (dec (z2 = 0)) as [E4 | E4]|];simpl. + apply ap. apply Sigma.path_sigma_hprop. simpl. rewrite PathGroupoids.transport_const. rewrite <-E1,<-E3,E4,plus_0_r in E. apply (left_cancellation plus (na+pb)). rewrite plus_0_r. path_via (pb + z1 + na). ring_with_nat. + destruct E4. rewrite <-E1,<-E3 in E. assert (Hrw : pb + z1 + (na + z2) = (na + pb) + (z1 + z2)) by ring_with_nat. rewrite <-(plus_0_r (na+pb)),Hrw in E. apply (left_cancellation _ _),naturals.zero_sum in E. apply E. + apply ap,Sigma.path_sigma_hprop. simpl. rewrite PathGroupoids.transport_const. rewrite <-E1,<-E3 in E. apply (left_cancellation plus (pb+nb)). path_via (pb + z1 + nb);[|path_via (nb + z2 + pb)];ring_with_nat. Qed.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals