module ExpRenSub where data Bool : Set where tt : Bool ff : Bool if_then_else_ : {A : Set} → Bool → A → A → A if tt then x else _ = x if ff then _ else y = y data Nat : Set where z : Nat s : Nat → Nat _+_ : Nat → Nat → Nat z + n = n s m + n = s (m + n) data Fin : Nat → Set where z : ∀{n} → Fin (s n) s : ∀{n} → Fin n → Fin (s n) data Exp (n : Nat) : Set where nval : Nat → Exp n bval : Bool → Exp n if : Bool → Exp n → Exp n → Exp n var : Fin n → Exp n add : Exp n → Exp n → Exp n Ren : Nat → Nat → Set Ren m n = Fin m → Fin n ren : {m n : Nat} → Ren m n → Exp m → Exp n ren f (nval n) = nval n ren f (bval b) = bval b ren f (if b e1 e2) = if b (ren f e1) (ren f e2) ren f (var i) = var (f i) ren f (add e1 e2) = add (ren f e1) (ren f e2) idRen : ∀{n} → Ren n n idRen i = i compRen : ∀{m n o} → Ren n o → Ren m n → Ren m o compRen f g i = f (g i) data _≅_ {A : Set} : A → A → Set where refl : {a : A} → a ≅ a resp2 : {A B C : Set}(f : A → B → C){a a' : A} → a ≅ a' → {b b' : B} → b ≅ b' → f a b ≅ f a' b' resp2 f refl refl = refl renid : ∀{n}(e : Exp n) → ren idRen e ≅ e renid (nval n) = refl renid (bval b) = refl renid (if b e0 e1) = resp2 (if b) (renid e0) (renid e1) renid (var i) = refl renid (add e0 e1) = resp2 add (renid e0) (renid e1) rencomp : ∀{m n o}(e : Exp m)(f : Ren n o)(g : Ren m n) → ren (compRen f g) e ≅ ren f (ren g e) rencomp (nval n) f g = refl rencomp (bval b) f g = refl rencomp (if b e0 e1) f g = resp2 (if b) (rencomp e0 f g) (rencomp e1 f g) rencomp (var i) f g = refl rencomp (add e0 e1) f g = resp2 add (rencomp e0 f g) (rencomp e1 f g) Sub : Nat → Nat → Set Sub m n = Fin m → Exp n sub : ∀{m n} → Sub m n → Exp m → Exp n sub f (nval n) = nval n sub f (bval b) = bval b sub f (if b e0 e1) = if b (sub f e0) (sub f e1) sub f (var i) = f i sub f (add e0 e1) = add (sub f e0) (sub f e1) idSub : ∀{n} → Sub n n idSub = var compSub : ∀{m n o} → Sub n o → Sub m n → Sub m o compSub f g i = sub f (g i) subid : ∀{n}(e : Exp n) → sub idSub e ≅ e subid (nval n) = refl subid (bval b) = refl subid (if b e0 e1) = resp2 (if b) (subid e0) (subid e1) subid (var i) = refl subid (add e0 e1) = resp2 add (subid e0) (subid e1) subcomp : ∀{m n o}(e : Exp m)(f : Sub n o)(g : Sub m n) → sub (compSub f g) e ≅ sub f (sub g e) subcomp (nval n) f g = refl subcomp (bval b) f g = refl subcomp (if b e0 e1) f g = resp2 (if b) (subcomp e0 f g) (subcomp e1 f g) subcomp (var i) f g = refl subcomp (add e0 e1) f g = resp2 add (subcomp e0 f g) (subcomp e1 f g)