[Dropped the assumption of extensionality.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20091119140846
 Ignore-this: 31da99d3fd9cd3e61109c542d581a997
] hunk ./CompositionBased.agda 5
-open import Relation.Binary.HeterogeneousEquality as HE
-  using (_≅_; refl)
-
-module CompositionBased
-         -- Extensionality is assumed. (This is probably not
-         -- necessary.)
-         (ext : ∀ {A B C : Set} {f : A → B} {g : A → C} →
-                  (∀ x → f x ≅ g x) → f ≅ g)
-         where
+module CompositionBased where
hunk ./CompositionBased.agda 11
+open ≡-Reasoning
hunk ./CompositionBased.agda 14
-import ReverseComposition
-open ReverseComposition ext
+open import ReverseComposition
hunk ./CompositionBased.agda 36
-  open ≡-Reasoning
-
hunk ./CompositionBased.agda 60
-  open HE.≅-Reasoning
hunk ./CompositionBased.agda 71
-    eval (val n)   i f = ▶ begin 0 ∣ i ∣ return n ⊙ f ∎
-    eval (e₁ ⊖ e₂) i f = ▶ begin
-      0 ∣ i ∣ (0 ∣ 0 ∣ ⟦ e₂ ⟧C ⊙ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub)) ⊙ f    ≅⟨ assoc 0 0 i ⟦ e₂ ⟧C (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub) f  ⟩
-      0 ∣ i ∣ ⟦ e₂ ⟧C ⊙ (1 ∣ i ∣ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub) ⊙ f)    ≅⟨ HE.cong (_∣_∣_⊙_ 0 i ⟦ e₂ ⟧C)
-                                                                               (assoc 0 1 i ⟦ e₁ ⟧C sub f) ⟩
+    eval (val n)   i f = ▷ begin 0 ∣ i ∣ return n ⊙ f ∎
+    eval (e₁ ⊖ e₂) i f = ▷ begin
+      0 ∣ i ∣ (0 ∣ 0 ∣ ⟦ e₂ ⟧C ⊙ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub)) ⊙ f    ≡⟨ refl ⟩
+      0 ∣ i ∣ ⟦ e₂ ⟧C ⊙ (1 ∣ i ∣ (0 ∣ 1 ∣ ⟦ e₁ ⟧C ⊙ sub) ⊙ f)    ≡⟨ refl ⟩
hunk ./CompositionBased.agda 84
-  correct e = halt , HE.≅-to-≡ (begin
+  correct e = halt , (begin
hunk ./CompositionBased.agda 86
-    ⟦ e ⟧C                 ≅⟨ HE.sym $ right-identity 0 ⟦ e ⟧C ⟩
+    ⟦ e ⟧C                 ≡⟨ refl ⟩
hunk ./CompositionBased.agda 97
-  open ≡-Reasoning
hunk ./ReverseComposition.agda 5
-open import Relation.Binary.HeterogeneousEquality using (_≅_; refl)
-
-module ReverseComposition
-         -- Extensionality is assumed. (This is probably not
-         -- necessary.)
-         (ext : ∀ {A B C : Set} {f : A → B} {g : A → C} →
-                  (∀ x → f x ≅ g x) → f ≅ g)
-         where
+module ReverseComposition where
hunk ./ReverseComposition.agda 7
+open import Data.Empty
hunk ./ReverseComposition.agda 10
+open import Relation.Binary.PropositionalEquality
hunk ./ReverseComposition.agda 12
-infixr 5 _∣_∣_⊙_
+------------------------------------------------------------------------
+-- N-ary functions
+
hunk ./ReverseComposition.agda 21
+-- Heterogeneous equality.
+
+Eq : ∀ {A} m n → A ^ m → A ^ n → Set
+Eq zero    zero    x y = x ≡ y
+Eq zero    (suc n) f g = ⊥
+Eq (suc m) zero    f g = ⊥
+Eq (suc m) (suc n) f g = ∀ x → Eq m n (f x) (g x)
+
+reflexive : ∀ {A} n {f : A ^ n} → Eq n n f f
+reflexive zero    = refl
+reflexive (suc n) = λ _ → reflexive n
+
+------------------------------------------------------------------------
+-- Generalised reverse composition
+
+infixr 5 _∣_∣_⊙_
+
hunk ./ReverseComposition.agda 45
-        i + j ∣ k ∣ i ∣ j ∣ f ⊙ g ⊙ h ≅
-        i ∣ j + k ∣ f ⊙ suc j ∣ k ∣ g ⊙ h
-assoc zero    j k x g h = refl
-assoc (suc i) j k f g h = ext λ x → assoc i j k (f x) g h
+        Eq (i + j + k) (i + (j + k))
+           (i + j ∣ k ∣ i ∣ j ∣ f ⊙ g ⊙ h)
+           (i ∣ j + k ∣ f ⊙ suc j ∣ k ∣ g ⊙ h)
+assoc zero    j k x g h = reflexive (j + k)
+assoc (suc i) j k f g h = λ x → assoc i j k (f x) g h
hunk ./ReverseComposition.agda 51
-right-identity : ∀ {A} i (f : A ^ i) → i ∣ 0 ∣ f ⊙ id ≅ f
+right-identity : ∀ {A} i (f : A ^ i) → Eq (i + 0) i (i ∣ 0 ∣ f ⊙ id) f
hunk ./ReverseComposition.agda 53
-right-identity (suc i) f = ext λ x → right-identity i (f x)
+right-identity (suc i) f = λ x → right-identity i (f x)
hunk ./ReverseComposition.agda 55
-left-identity : ∀ {A} i (f : A ^ suc i) → 1 ∣ i ∣ id ⊙ f ≅ f
-left-identity zero    f = refl
-left-identity (suc i) f = ext λ x → left-identity i (f x)
+left-identity : ∀ {A} i (f : A ^ suc i) →
+                Eq (suc i) (suc i) (1 ∣ i ∣ id ⊙ f) f
+left-identity i f = λ _ → reflexive i