Is unguarded fixpoint reduction consistent?

Question

In Coq, there are two restrictions on fixpoints to retain normalization:

1. Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and
2. Reduction occurs only when applied to a constructor in the recursive argument position (also called guarded recursion, apparently).

Evidently, without #1 you could prove an inconsistency and break normalization, e.g. fix f (n: nat) (A: Type): A := f (S n) A, while without #2 you could unfold a fixpoint indefinitely (reducing under lambdas and such). Does removing only #2 also break consistency, or merely normalization? I'm wondering if you could have a consistent type theory with an equality rule like

$$ \Gamma, f: A \vdash e: A \\ \rule{19em}{1px}. \\ \Gamma \vdash (\mathrm{fix} \: f : A := e) \equiv e[f/(\mathrm{fix} \: f : A := e)] : A $$

Answer 1

This is consistent.

First, this equality holds propositionally by eta-expansion of the constructor. Thus, if your type theory had equality reflection, it would also hold definitionally. Since Extensional Type Theory is consistent, this rule also is.