@~ is coercion application.
The angle brackets denote a reflexive coercion of their contained type with role given by the underscored letter.
Thus <Nat.Flip x_ap0H>_N is an equality proof that Nat.Flip x_apH is equal to Nat.Flip x_apH nominally (as equal types not just equal representations).
PS has a lot of arguments. We look at the smart constructor $WPS and we can see the first two are the types of x and y respectively. We have proof that the constructor argument is Flip x (in this case we have Flip x ~ Even. We then have the proofs x ~ Flip y and y ~ Flip x. The final argument is a value of ParNat x.
I will now walk through the first cast of type Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd
We start with (Nat.ParNat ...)_R. This is a type constructor application. It lifts the proof of x_aIX ~# 'Nat.Odd to Nat.ParNat x_aIX ~# Nat.ParNat 'Nat.Odd. The R means it does this representationally meaning that the types are isomorphic but not the same (in this case they are the same but we don’t need that knowledge to perform the cast).
Now we look at main body of the proof (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]). ; means transitivty i.e. apply these proofs in order.
dt1_dK7 is a proof of x_aIX ~# Nat.Flip y_aIY.
If we look at (dt2_dK8 ; Sym dt_dK6). dt2_dK8 shows y_aIY ~# Nat.Flip x_aIX. dt_dK6 is of type 'Nat.Even ~# Nat.Flip x_aIX. So Sym dt_dK6 is of type Nat.Flip x_aIX ~# 'Nat.Even and (dt2_dK8 ; Sym dt_dK6) is of type y_aIY ~# 'Nat.Even
Thus (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N is a proof that Nat.Flip y_aIY ~# Nat.Flip 'Nat.Even.
Nat.TFCo:R:Flip[0] is the first rule of flip which is Nat.Flip 'Nat.Even ~# 'Nat.Odd' .
Putting these together we get (dt1_dK7 ; (Nat.Flip (dt2_dK8 ; Sym dt_dK6))_N; Nat.TFCo:R:Flip[0]) has type x_aIX #~ 'Nat.Odd.
The second more complicated cast is a bit harder to work out but should work on the same principle.