Casting a value from one fintype to another?

Being a Coq newbie, I am stuck on this problem. Hopefully, someone can help!

Given an encoding of finite types in Coq as below -

Fixpoint fin (n : nat) : Type :=
  match n with
  | 0 => False
  | S m => option (fin m)
  end.

Is it possible to define a function that lifts a value from fin (S n) to fin (S (S n)), while keeping the value the same. Thus, I am hoping to have the following equalities such as -

@up 2 (None : fin 2) = (None : fin 3)

@up 2 (Some None : fin 2) = (Some None : fin 3)

I thought of writing this -

Fixpoint up {n:nat} : fin (S n) -> fin (S (S n)) :=
fun p => match p with 
         | None => None 
         | Some p' => Some (up p)

But it is rejected. Intuitively I understand that it is possible because - members of fin 2 - None, Some None are members of fin 3 - None, Some None, Some (Some None) and so on. But I am not able to write the function for the same. I suspect its because the recursive definition has to deal with @up 0 where there should be an empty match, but I am not sure how to write this case. Any help would be appreciated! Thanks

You will need dependent pattern matching for your term to type-check properly.

Your structural parameter can only be n because this is the sole parameter of your Fixpoint. Your recursive call must be applied on a sub-term of n so you need a match on n somewhere.

I would favor the solution below, of return type fin n -> fin (S n), which is a bit more general, but you can specialize it to fin (S n) -> fin (S (S n)) later on of needed:

Fixpoint up {n} : fin n -> fin (S n) :=
  match n return fin n -> fin (S n) with 
  | 0   => fun p => match p with end
  | S n => fun p => match p with 
                    | None => None
                    | Some q => Some (up q)
                    end
  end.

Goal forall n, @up (S n) None = None.
Proof. reflexivity. Qed.

Goal forall n (p : fin n), @up (S n) (Some p) = Some (up p).
Proof. reflexivity. Qed.

Fixpoint fin2nat {n} : fin n -> nat :=
  match n with 
  | 0   => fun p => match p with end
  | S n => fun p => match p with
                    | None   => 0
                    | Some p => S (fin2nat p)
                    end
  end.

Eval compute in @fin2nat 8 (Some (Some (Some None))).
Eval compute in @fin2nat 20 (Some (Some (Some None))).

Fact up_correct {n} p : fin2nat (@up n p) = fin2nat p.
Proof.
  induction n as [ | n IHn ] in p |- *; destruct p; simpl fin2nat; trivial.
  f_equal; exact (IHn _).
Qed.