How to express an axiom as a sigma type? (translating Agda)

Stream: new members

[nrs]

I have the following bit of Agda I'm trying to express in Lean:

data _->>_ : Term → Term → Set where
  _∎ : ∀ M
      ---------
    → M ->> M

  step—→ : ∀ L {M N}
    → M ->> N
    → L !> M
      ---------
    → L ->> N

postulate
  confluence : ∀ {L M N}
    → ((L ->> M) × (L ->> N))
      --------------------
    → ∃[ P ] ((M ->> P) × (N ->> P))

(from https://plfa.github.io/Lambda/)
What I've come up with is:

inductive pclos : Term -> Term -> Prop where
  | clos : pclos M M
  | step : pclos M N -> pclos L M -> pclos L N

axiom confluence {L M N : Term} : (pclos L M) ∧ (pclos L N) -> ∃ P : Term, (pclos M P) ∧ (pclos N P)

But it bothers me that Agda's expression seems to be closer to the type-theoretical notion of existentials since it maps to Set instead of to Prop, and seems to express the axiom purely as a type instead of a proposition. Would there be a way to do the same in Lean, maybe using sigma types?

[Kyle Miller]

In Lean you can use Term -> Term -> Type if you want the inductive to be type-valued, and to turn it back into a prop for the existential you can write Nonempty (pclos M P) for example.

You can also factor the Nonemptys out of the Exists to form the equivalent Nonempty (Σ P : Term, pclos M P × pclos N P)

[Kyle Miller]

(Note: in your step, the second pclos should be the type for the reduction rule https://plfa.github.io/Lambda/#plfa_plfa-part2-Lambda-20283)

[nrs]

Kyle Miller said:

In Lean you can use Term -> Term -> Type if you want the inductive to be type-valued, and to turn it back into a prop for the existential you can write Nonempty (pclos M P) for example.

You can also factor the Nonemptys out of the Exists to form the equivalent Nonempty (Σ P : Term, pclos M P × pclos N P)

Thanks for the answer (and the note)! In your opinion, would it make more sense then to express the axiom using Nonempty, or is there a way to express the axiom as a function with -> between Type-level expressions? Otherwise, expressed using Nonempty, the axiom would just be a Prop, right?

[Kyle Miller]

I'm not sure. I suppose you could write it as

axiom confluence {L M N : Term} : pclos L M -> pclos L N -> Σ P : Term, pclos M P × pclos N P

if you think it makes sense that there could be a function that computes this P. If not, then I'm not sure it makes any real difference (you could "compute" the P for an existential using choice).

[nrs]

Kyle Miller said:

I'm not sure. I suppose you could write it as

axiom confluence {L M N : Term} : pclos L M -> pclos L N -> Σ P : Term, pclos M P × pclos N P

if you think it makes sense that there could be a function that computes this P. If not, then I'm not sure it makes any real difference (you could "compute" the P for an existential using choice).

I see, thanks a lot for the help!