open import Definition.Typed.Restrictions
import Graded.Modality
module Graded.Modality.Instances.Examples
{a} {M : Set a}
(open Graded.Modality M)
{π : Modality}
(open Modality π)
(R : Type-restrictions π)
(open Type-restrictions R)
(Ξ -π-π : Ξ -allowed π π)
where
open import Tools.Fin
open import Tools.Function
import Tools.Reasoning.PartialOrder
open import Definition.Typed R
open import Definition.Untyped M
private
β’β : β’ Ξ΅ β β
β’β = Ξ΅ β ββ±Ό Ξ΅
β’ββ : β’ Ξ΅ β β β β
β’ββ = β’β β ββ±Ό β’β
β’βββ : β’ Ξ΅ β β β β β β
β’βββ = β’ββ β ββ±Ό β’ββ
β’ββββ : β’ Ξ΅ β β β β β β β β
β’ββββ = β’βββ β ββ±Ό β’βββ
double : Term 0
double = lam π (natrec π π π β (var x0) (suc (var x0)) (var x0))
β’double : Ξ΅ β’ double β· Ξ π , π β· β βΉ β
β’double =
flip (lamβ±Ό (ββ±Ό Ξ΅)) Ξ -π-π $
natrecβ±Ό (ββ±Ό β’ββ) (var β’β here)
(sucβ±Ό (var β’βββ here))
(var β’β here)
plus : Term 0
plus = lam π $ lam π $ natrec π π π β (var x0) (suc (var x0)) (var x1)
β’plus : Ξ΅ β’ plus β· Ξ π , π β· β βΉ Ξ π , π β· β βΉ β
β’plus =
flip (lamβ±Ό (ββ±Ό Ξ΅)) Ξ -π-π $
flip (lamβ±Ό (ββ±Ό β’β)) Ξ -π-π $
natrecβ±Ό (ββ±Ό β’βββ) (var β’ββ here)
(sucβ±Ό (var β’ββββ here))
(var β’ββ (there here))