Compliance/Equality

parent 725e7368
......@@ -53,7 +53,7 @@ infixl 3 _⫃[_]_
%<*implements-pointwise>
\AgdaTarget{\_⫃[\_]\_}
\begin{code}
_⫃[_]_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → W⟶W i o → Set
_⫃[_]_ : ∀ {i o G} (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i o) → Set
c ⫃[ g ] f = ∀ w → c ⫃[ g ] f at w
\end{code}
%</implements-pointwise>
......@@ -97,7 +97,7 @@ c ⫃[ g ] f = ∀ w → c ⫃[ g ] f at w
%<*implements-semihet-at>
\AgdaTarget{\_⫅[\_]\_at\_}
\begin{code}
_⫅[_]_at_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → W⟶W i o′ → (W i → Set)
_⫅[_]_at_ : ∀ {i o o′ G} (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i o′) → (W i → Set)
c ⫅[ g ] f at w = ⟦ c ⟧[ g ] w ≈ f w
\end{code}
%</implements-semihet-at>
......@@ -109,7 +109,7 @@ infixl 3 _⫅[_]_
%<*implements-semihet>
\AgdaTarget{\_⫅[\_]\_}
\begin{code}
_⫅[_]_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → W⟶W i o′ → Set
_⫅[_]_ : ∀ {i o o′ G} (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i o′) → Set
c ⫅[ g ] f = ∀ w → c ⫅[ g ] f at w
\end{code}
%</implements-semihet>
......@@ -153,7 +153,7 @@ c ⫅[ g ] f = ∀ w → c ⫅[ g ] f at w
%<*implements-preserve-semihet-at>
\AgdaTarget{\_⫇[\_]\_at\_/\_}
\begin{code}
_⫇[_]_at_/_ : ∀ {i o i′ o′ G} → ℂ[ G ] i o → TyGate G W⟶W → W⟶W i′ o′ → (W i → W i′ → Set)
_⫇[_]_at_/_ : ∀ {i o i′ o′ G} (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i′ o′) → (W i → W i′ → Set)
c ⫇[ g ] f at w / w′ = w ≈ w′ → ⟦ c ⟧[ g ] w ≈ f w′
\end{code}
%</implements-preserve-semihet-at>
......@@ -165,7 +165,7 @@ infixl 3 _⫇[_]_
%<*implements-preserve-semihet>
\AgdaTarget{\_⫇[\_]\_}
\begin{code}
_⫇[_]_ : ∀ {i o i′ o′ G} → ℂ[ G ] i o → TyGate G W⟶W → W⟶W i′ o′ → Set
_⫇[_]_ : ∀ {i o i′ o′ G} (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i′ o′) → Set
c ⫇[ g ] f = ∀ {w w′} → c ⫇[ g ] f at w / w′
\end{code}
%</implements-preserve-semihet>
......@@ -225,7 +225,7 @@ infixl 3 _⫉[_]_
%<*implements>
\AgdaTarget{\_⫉[\_]\_}
\begin{code}
data _⫉[_]_ {i o i′ o′ G} : ℂ[ G ] i o → TyGate G W⟶W → W⟶W i′ o′ → Set where
data _⫉[_]_ {i o i′ o′ G} : (c : ℂ[ G ] i o) (g : TyGate G W⟶W) (f : W⟶W i′ o′) → Set where
refl⫉ : {c : ℂ[ G ] i o} {f : W⟶W i′ o′} {g : TyGate G W⟶W} (i≡ : i ≡ i′) → c ⫇[ g ] f → c ⫉[ g ] f
\end{code}
%</implements>
......@@ -268,7 +268,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-pointwise-at-with-gates>
\AgdaTarget{\_⫃\_at\_}
\begin{code}
_⫃_at_ : ∀ {i o} → ℂ[ G ] i o → W⟶W i o → (W i → Set)
_⫃_at_ : ∀ {i o} (c : ℂ[ G ] i o) (f : W⟶W i o) → (W i → Set)
_⫃_at_ = _⫃[ g ]_at_
\end{code}
%</implements-pointwise-at-with-gates>
......@@ -280,7 +280,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-pointwise-with-gates>
\AgdaTarget{\_⫃\_}
\begin{code}
_⫃_ : ∀ {i o} → ℂ[ G ] i o → W⟶W i o → Set
_⫃_ : ∀ {i o} (c : ℂ[ G ] i o) (f : W⟶W i o) → Set
_⫃_ = _⫃[ g ]_
\end{code}
%</implements-pointwise-with-gates>
......@@ -321,7 +321,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-semihet-at-with-gates>
\AgdaTarget{\_⫅\_at\_}
\begin{code}
_⫅_at_ : ∀ {i o o′} → ℂ[ G ] {σ} i o → W⟶W i o′ → (W i → Set)
_⫅_at_ : ∀ {i o o′} (c : ℂ[ G ] {σ} i o) (f : W⟶W i o′) → (W i → Set)
_⫅_at_ = _⫅[ g ]_at_
\end{code}
%</implements-semihet-at-with-gates>
......@@ -333,7 +333,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-semihet-with-gates>
\AgdaTarget{\_⫅\_}
\begin{code}
_⫅_ : ∀ {i o o′} → ℂ[ G ] {σ} i o → W⟶W i o′ → Set
_⫅_ : ∀ {i o o′} (c : ℂ[ G ] {σ} i o) (f : W⟶W i o′) → Set
_⫅_ = _⫅[ g ]_
\end{code}
%</implements-semihet-with-gates>
......@@ -374,7 +374,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-preserve-semihet-at-with-gates>
\AgdaTarget{\_⫇\_at\_/\_}
\begin{code}
_⫇_at_/_ : ∀ {i o i′ o′} → ℂ[ G ] i o → W⟶W i′ o′ → (W i → W i′ → Set)
_⫇_at_/_ : ∀ {i o i′ o′} (c : ℂ[ G ] i o) (f : W⟶W i′ o′) → (W i → W i′ → Set)
_⫇_at_/_ = _⫇[ g ]_at_/_
\end{code}
%</implements-preserve-semihet-at-with-gates>
......@@ -386,7 +386,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-preserve-semihet-with-gates>
\AgdaTarget{\_⫇\_}
\begin{code}
_⫇_ : ∀ {i o i′ o′} → ℂ[ G ] i o → W⟶W i′ o′ → Set
_⫇_ : ∀ {i o i′ o′} (c : ℂ[ G ] i o) (f : W⟶W i′ o′) → Set
_⫇_ = _⫇[ g ]_
\end{code}
%</implements-preserve-semihet-with-gates>
......@@ -431,7 +431,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*implements-with-gates>
\AgdaTarget{\_⫉\_}
\begin{code}
_⫉_ : ∀ {i o i′ o′} → ℂ[ G ] i o → W⟶W i′ o′ → Set
_⫉_ : ∀ {i o i′ o′} (c : ℂ[ G ] i o) (f : W⟶W i′ o′) → Set
_⫉_ = _⫉[ g ]_
\end{code}
%</implements-with-gates>
......@@ -41,7 +41,7 @@ reindex-setoid s f = record { Carrier = Carrier₀ ∘′ f
%<*eq-pointwise-at>
\AgdaTarget{\_≗[\_]\_at\_}
\begin{code}
_≗[_]_at_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → (W i → Set)
_≗[_]_at_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → (W i → Set)
c₁ ≗[ g ] c₂ at w = c₁ ⫃[ g ] ⟦ c₂ ⟧[ g ] at w
\end{code}
%</eq-pointwise-at>
......@@ -53,7 +53,7 @@ infix 3 _≗[_]_
%<*eq-pointwise>
\AgdaTarget{\_≗[\_]\_}
\begin{code}
_≗[_]_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → Set
_≗[_]_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → Set
c₁ ≗[ g ] c₂ = c₁ ⫃[ g ] ⟦ c₂ ⟧[ g ]
\end{code}
%</eq-pointwise>
......@@ -62,7 +62,7 @@ c₁ ≗[ g ] c₂ = c₁ ⫃[ g ] ⟦ c₂ ⟧[ g ]
%<*eq-pointwise-c-at>
\AgdaTarget{\_≗ᶜ[\_]\_at\_}
\begin{code}
_≗ᶜ[_]_at_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → (Γᶜ (W i) → Set)
_≗ᶜ[_]_at_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → (Γᶜ (W i) → Set)
c₁ ≗ᶜ[ g ] c₂ at γ = ⟦ c₁ ⟧ᶜ[ g ] γ ≡ ⟦ c₂ ⟧ᶜ[ g ] γ
\end{code}
%</eq-pointwise-c-at>
......@@ -74,7 +74,7 @@ infix 3 _≗ᶜ[_]_
%<*eq-pointwise-c>
\AgdaTarget{\_≗ᶜ[\_]\_}
\begin{code}
_≗ᶜ[_]_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → Set
_≗ᶜ[_]_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → Set
c₁ ≗ᶜ[ g ] c₂ = ∀ γ → c₁ ≗ᶜ[ g ] c₂ at γ
\end{code}
%</eq-pointwise-c>
......@@ -83,7 +83,7 @@ c₁ ≗ᶜ[ g ] c₂ = ∀ γ → c₁ ≗ᶜ[ g ] c₂ at γ
%<*eq-pointwise-omega-at>
\AgdaTarget{\_≗ω[\_]\_at\_}
\begin{code}
_≗ω[_]_at_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → (Stream (W i) → Set)
_≗ω[_]_at_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → (Stream (W i) → Set)
c₁ ≗ω[ g ] c₂ at ins = ⟦ c₁ ⟧ω[ g ] ins ≈ₛ ⟦ c₂ ⟧ω[ g ] ins
\end{code}
%</eq-pointwise-omega-at>
......@@ -95,7 +95,7 @@ infix 3 _≗ω[_]_
%<*eq-pointwise-omega>
\AgdaTarget{\_≗ω[\_]\_}
\begin{code}
_≗ω[_]_ : ∀ {i o G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o → Set
_≗ω[_]_ : ∀ {i o G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o) → Set
c₁ ≗ω[ g ] c₂ = ∀ ins → c₁ ≗ω[ g ] c₂ at ins
\end{code}
%</eq-pointwise-omega>
......@@ -105,7 +105,7 @@ c₁ ≗ω[ g ] c₂ = ∀ ins → c₁ ≗ω[ g ] c₂ at ins
%<*eq-semihet-at>
\AgdaTarget{\_≅[\_]\_at\_}
\begin{code}
_≅[_]_at_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o′ → (W i → Set)
_≅[_]_at_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o′) → (W i → Set)
c₁ ≅[ g ] c₂ at w = c₁ ⫅[ g ] ⟦ c₂ ⟧[ g ] at w
\end{code}
%</eq-semihet-at>
......@@ -117,7 +117,7 @@ infix 3 _≅[_]_
%<*eq-semihet>
\AgdaTarget{\_≅[\_]\_}
\begin{code}
_≅[_]_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o′ → Set
_≅[_]_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o′) → Set
c₁ ≅[ g ] c₂ = c₁ ⫅[ g ] ⟦ c₂ ⟧[ g ]
\end{code}
%</eq-semihet>
......@@ -126,7 +126,7 @@ c₁ ≅[ g ] c₂ = c₁ ⫅[ g ] ⟦ c₂ ⟧[ g ]
%<*eq-semihet-c-at>
\AgdaTarget{\_≅ᶜ[\_]\_at\_}
\begin{code}
_≅ᶜ[_]_at_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o′ → (Γᶜ (W i) → Set)
_≅ᶜ[_]_at_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o′) → (Γᶜ (W i) → Set)
c₁ ≅ᶜ[ g ] c₂ at γ = ⟦ c₁ ⟧ᶜ[ g ] γ ≈ ⟦ c₂ ⟧ᶜ[ g ] γ
\end{code}
%</eq-semihet-c-at>
......@@ -138,7 +138,7 @@ infix 3 _≅ᶜ[_]_
%<*eq-semihet-c>
\AgdaTarget{\_≅ᶜ[\_]\_}
\begin{code}
_≅ᶜ[_]_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o′ → Set
_≅ᶜ[_]_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o′) → Set
c₁ ≅ᶜ[ g ] c₂ = ∀ γ → c₁ ≅ᶜ[ g ] c₂ at γ
\end{code}
%</eq-semihet-c>
......@@ -147,7 +147,7 @@ c₁ ≅ᶜ[ g ] c₂ = ∀ γ → c₁ ≅ᶜ[ g ] c₂ at γ
%<*eq-semihet-omega-at>
\AgdaTarget{\_≅ᶜ[\_]\_at\_}
\begin{code}
_≅ω[_]_at_ : ∀ {i o o′ G} → ℂ[ G ] {ω} i o → TyGate G W⟶W → ℂ[ G ] {ω} i o′ → (Stream (W i) → Set)
_≅ω[_]_at_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] {ω} i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] {ω} i o′) → (Stream (W i) → Set)
c₁ ≅ω[ g ] c₂ at ins = ⊥ where postulate ⊥ : _ -- ⟦ c₁ ⟧ω[ g ] ins ≈ₛ {- TODO -} ⟦ c₂ ⟧ω[ g ] ins
\end{code}
%</eq-semihet-omega-at>
......@@ -159,7 +159,7 @@ infix 3 _≅ω[_]_
%<*eq-semihet-omega>
\AgdaTarget{\_≅ω[\_]\_}
\begin{code}
_≅ω[_]_ : ∀ {i o o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i o′ → Set
_≅ω[_]_ : ∀ {i o o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i o′) → Set
c₁ ≅ω[ g ] c₂ = ∀ ins → c₁ ≅ω[ g ] c₂ at ins
\end{code}
%</eq-semihet-omega>
......@@ -169,7 +169,7 @@ c₁ ≅ω[ g ] c₂ = ∀ ins → c₁ ≅ω[ g ] c₂ at ins
%<*eq-preserve-semihet-at>
\AgdaTarget{\_≊[\_]\_at\_/\_}
\begin{code}
_≊[_]_at_/_ : ∀ {i o i′ o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i′ o′ → (W i → W i′ → Set)
_≊[_]_at_/_ : ∀ {i o i′ o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i′ o′) → (W i → W i′ → Set)
c₁ ≊[ g ] c₂ at w / w′ = c₁ ⫇[ g ] ⟦ c₂ ⟧[ g ] at w / w′
\end{code}
%</eq-preserve-semihet-at>
......@@ -181,7 +181,7 @@ infix 3 _≊[_]_
%<*eq-preserve-semihet>
\AgdaTarget{\_≊[\_]\_}
\begin{code}
_≊[_]_ : ∀ {i o i′ o′ G} → ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i′ o′ → Set
_≊[_]_ : ∀ {i o i′ o′ G} (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i′ o′) → Set
c₁ ≊[ g ] c₂ = c₁ ⫇[ g ] ⟦ c₂ ⟧[ g ]
\end{code}
%</eq-preserve-semihet>
......@@ -244,7 +244,7 @@ infix 3 _≋[_]_
%<*eq>
\AgdaTarget{\_≋[\_]\_}
\begin{code}
data _≋[_]_ {i o i′ o′ G} : ℂ[ G ] i o → TyGate G W⟶W → ℂ[ G ] i′ o′ → Set where
data _≋[_]_ {i o i′ o′ G} : (c₁ : ℂ[ G ] i o) (g : TyGate G W⟶W) (c₂ : ℂ[ G ] i′ o′) → Set where
refl≋ : {c₁ : ℂ[ G ] i o} {c₂ : ℂ[ G ] i′ o′} {g : TyGate G W⟶W} (i≡ : i ≡ i′) → c₁ ≊[ g ] c₂ → c₁ ≋[ g ] c₂
\end{code}
%</eq>
......@@ -351,7 +351,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-pointwise-at-with-gates>
\AgdaTarget{\_≗\_at\_}
\begin{code}
_≗_at_ : ∀ {i o} → ℂ[ G ] i o → ℂ[ G ] i o → (W i → Set)
_≗_at_ : ∀ {i o} (c₁ c₂ : ℂ[ G ] i o) → (W i → Set)
_≗_at_ = _≗[ g ]_at_
\end{code}
%</eq-pointwise-at-with-gates>
......@@ -363,7 +363,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-pointwise-with-gates>
\AgdaTarget{\_≗\_}
\begin{code}
_≗_ : ∀ {i o} → ℂ[ G ] i o → ℂ[ G ] i o → Set
_≗_ : ∀ {i o} (c₁ c₂ : ℂ[ G ] i o) → Set
_≗_ = _≗[ g ]_
\end{code}
%</eq-pointwise-with-gates>
......@@ -404,7 +404,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-semihet-at-with-gates>
\AgdaTarget{\_≅\_at\_}
\begin{code}
_≅_at_ : ∀ {i o o′} → ℂ[ G ] i o → ℂ[ G ] i o′ → (W i → Set)
_≅_at_ : ∀ {i o o′} (c₁ : ℂ[ G ] i o) (c₂ : ℂ[ G ] i o′) → (W i → Set)
_≅_at_ = _≅[ g ]_at_
\end{code}
%</eq-semihet-at-with-gates>
......@@ -416,7 +416,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-semihet-with-gates>
\AgdaTarget{\_≅\_}
\begin{code}
_≅_ : ∀ {i o o′} → ℂ[ G ] i o → ℂ[ G ] i o′ → Set
_≅_ : ∀ {i o o′} (c₁ : ℂ[ G ] i o) (c₂ : ℂ[ G ] i o′) → Set
_≅_ = _≅[ g ]_
\end{code}
%</eq-semihet-with-gates>
......@@ -457,7 +457,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-preserve-semihet-at-with-gates>
\AgdaTarget{\_≊\_at\_/\_}
\begin{code}
_≊_at_/_ : ∀ {i o i′ o′} → ℂ[ G ] i o → ℂ[ G ] i′ o′ → (W i → W i′ → Set)
_≊_at_/_ : ∀ {i o i′ o′} (c₁ : ℂ[ G ] i o) (c₂ : ℂ[ G ] i′ o′) → (W i → W i′ → Set)
_≊_at_/_ = _≊[ g ]_at_/_
\end{code}
%</eq-preserve-semihet-at-with-gates>
......@@ -469,7 +469,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-preserve-semihet-with-gates>
\AgdaTarget{\_≊\_}
\begin{code}
_≊_ : ∀ {i o i′ o′} → ℂ[ G ] i o → ℂ[ G ] i′ o′ → Set
_≊_ : ∀ {i o i′ o′} (c₁ : ℂ[ G ] i o) (c₂ : ℂ[ G ] i′ o′) → Set
_≊_ = _≊[ g ]_
\end{code}
%</eq-preserve-semihet-with-gates>
......@@ -514,7 +514,7 @@ module WithGates {G} (g : TyGate G W⟶W) where
%<*eq-with-gates>
\AgdaTarget{\_≋\_}
\begin{code}
_≋_ : ∀ {i o i′ o′} → ℂ[ G ] i o → ℂ[ G ] i′ o′ → Set
_≋_ : ∀ {i o i′ o′} (c₁ : ℂ[ G ] i o) (c₂ : ℂ[ G ] i′ o′) → Set
_≋_ = _≋[ g ]_
\end{code}
%</eq-with-gates>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment