translation-mod

A coq plugin implementing the translation associated to a modality

Let ◯ be a strict modality.

To explain the translation on positive types as well, we also translate the sum type A + B, with associated constructors in_ℓ and in_r and eliminator ⟨_,_⟩. We note J the eliminator of the identity type.

• For types (assuming A ≠ Type)

• [Type] ≔ (Type^◯ ; π_Type^◯)

• We introduce the notation ⟦A⟧ ≔ π₁ [A]

• For dependent sums

• [Σ_x:A B] ≔ (Σ_x:⟦A⟧⟦B⟧, π_Σ^[A],[B])

• [(x,y)] ≔ ([x],[y])

• [π_i t] ≔ π_i [t]

• For dependent products

• [Π_x:A B] ≔ (Π_x:⟦A⟧⟦B⟧, π_Π^[A],[B])

• [λ x:A, M] ≔ λ x:⟦A⟧, [M]

• [t t'] ≔ [t] [t']

• For paths

• [A = B] ≔ ([A] = [B] ; π₌^[A],[B])

• [idpath] ≔ idpath

• [J] ≔ J

• For sums

• [A + B] ≔ (◯ ([|A|] + [|B|]) ; π_◯^[|A|]+[|B|])

• [in_ℓ t] ≔ η(in_ℓ [t])

• [in_r t] ≔ η(in_r [t])

• [⟨f,g⟩] ≔ ◯_rec^{⟦A⟧+⟦B⟧}⟨[f],[g]⟩

where π_Σ^A, B (resp. π_Π^A, B, resp. π₌^A, B) is the proof that Σ_x : AB (resp. ∏_x : AB, resp A = B) is modal as soon as A and B are, and π_◯^A a proof that ◯A is always modal.