```{-# OPTIONS --type-in-type  #-}

open import NeilPrelude

module TemporalFunction

(Time : Set)
(_<'_  : Rel Time)
(irreflex : Irreflexive _<'_)
(transit : Transitive _<'_)

where

-------------------------------------------------------

import TemporalLogic
open TemporalLogic Time _<'_ irreflex transit public

-------------------------------------------------------

infix 3 _≐_

-------------------------------------------------------

TVal : Set → Set
TVal A = Time → A

TFun : Set → Set → Set
TFun A B = TVal A → TVal B

-------------------------------------------------------

-- time varying equality

_≐_ : {A : Set} → TVal A → TVal A → TPred
(p ≐ q) t = p t ≡ q t

EqualTo : {A : Set} → TVal A → A → TPred
EqualTo s a t = s t ≡ a

EqualAt : {A : Set} → TVal A → Time → TPred
EqualAt s t = EqualTo s (s t)

-------------------------------------------------------

-- Properties of Temporal Functions

Contractive : {A B : Set} → TFun A B → Set
Contractive {A} f = (s₁ s₂ : TVal A) → Always (H (s₁ ≐ s₂) ⇒ f s₁ ≐ f s₂)

NonExpansive : {A B : Set} → TFun A B → Set
NonExpansive {A} f = (s₁ s₂ : TVal A) → Always (Hʳ (s₁ ≐ s₂) ⇒ f s₁ ≐ f s₂)

---------------------------------------------------------

lem-cont→nonexpansive : {A B : Set} → {f : TVal A → TVal B} → Contractive f → NonExpansive f
lem-cont→nonexpansive = result3' (argument snd)

lem-ne2 : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ Hʳ (b₁ ≐ b₂) ⇒ f (a₁ & b₁) ≐ f (a₂ & b₂))
lem-ne2 ne a₁ a₂ b₁ b₂ t (eqa , Heqa) (eqb , Heqb) = ne (a₁ & b₁) (a₂ & b₂) t (×-cong eqa eqb , ×-cong3 Heqa Heqb)

lem-H-cong : {A B : Set} → {f : TFun A B} → NonExpansive f → (s₁ s₂ : TVal A) → Always (H (s₁ ≐ s₂) ⇒ H (f s₁ ≐ f s₂))
lem-H-cong ne s₁ s₂ t Heq t' lt = ne s₁ s₂ t' (reduce-range-<-incl lt Heq)

lem-Hʳ : {A B : Set} → {f : TFun A B} → NonExpansive f → (s₁ s₂ : TVal A) → Always (Hʳ (s₁ ≐ s₂) ⇒ (f s₁ ≐ f s₂)) → Always (Hʳ (s₁ ≐ s₂) ⇒ Hʳ (f s₁ ≐ f s₂))
lem-Hʳ ne s₁ s₂ g t Heq = g t Heq , lem-H-cong ne s₁ s₂ t (snd Heq)

lem-Hʳ-cong2 : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ Hʳ (b₁ ≐ b₂) ⇒ f (a₁ & b₁) ≐ f (a₂ & b₂))
lem-Hʳ-cong2 ne a₁ a₂ b₁ b₂ t (eqa , Heqa) (eqb , Heqb) = ne (a₁ & b₁) (a₂ & b₂) t (×-cong eqa eqb , ×-cong3 Heqa Heqb)

lem-Hʳ-cong2L : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a : TVal A) → (b₁ b₂ : TVal B)
→ Always (Hʳ (b₁ ≐ b₂) ⇒ f (a & b₁) ≐ f (a & b₂))
lem-Hʳ-cong2L ne a b₁ b₂ t Heqb = lem-Hʳ-cong2 ne a a b₁ b₂ t (refl , λ _ _ → refl) Heqb

lem-Hʳ-cong2R : {A B C : Set} → {f : TFun (A × B) C} → NonExpansive f → (a₁ a₂ : TVal A) → (b : TVal B)
→ Always (Hʳ (a₁ ≐ a₂) ⇒ f (a₁ & b) ≐ f (a₂ & b))
lem-Hʳ-cong2R ne a₁ a₂ b t Heqa = lem-Hʳ-cong2 ne a₁ a₂ b b t Heqa (refl , λ _ _ → refl)

---------------------------------------------------------
```