[Made _⇨_ smaller and enabled η-equality for it. Nils Anders Danielsson **20101210193153 Ignore-this: 4b689c566412af546253a1ded8def24 + Took the opportunity to change the definition of _>>=∥_. ] hunk ./CompositionBased.agda 40 -_↑_ : Set → ℕ → Set₁ +_↑_ : Set → ℕ → Set hunk ./CompositionBased/Exceptions.agda 51 -_↑_ : Set → ℕ → Set₁ +_↑_ : Set → ℕ → Set hunk ./CompositionBased/Exceptions.agda 133 - (⟦ e₂ ⟧C ⊙M ⟦ e₁ ⟧C ⊙M C.sub) then s else f ≈⟨ distrib ⟦ e₂ ⟧C (_·_ (⟦ e₁ ⟧C ⊙M C.sub)) ⟩ + (⟦ e₂ ⟧C ⊙M ⟦ e₁ ⟧C ⊙M C.sub) then s else f ≈⟨ distrib ⟦ e₂ ⟧C (_·_ (⟦ e₁ ⟧C ⊙M C.sub)) (maybe s f) ⟩ hunk ./CompositionBased/Exceptions.agda 143 - else f ≈⟨ refl ⟦ e₂ ⟧C then (λ x → distrib ⟦ e₁ ⟧C (λ y → C.sub · y · x)) - else-cong refl f ⟩ + else f ≈⟨ refl ⟦ e₂ ⟧C + then (λ x → distrib ⟦ e₁ ⟧C (λ y → C.sub · y · x) (maybe s f)) + else-cong refl f ⟩ hunk ./CompositionBased/Exceptions.agda 173 - (⟦ e₁ ⟧C then returnM else ⟦ e₂ ⟧C) then s else f ≈⟨ distrib ⟦ e₁ ⟧C returnM ⟩ + (⟦ e₁ ⟧C then returnM else ⟦ e₂ ⟧C) then s else f ≈⟨ distrib ⟦ e₁ ⟧C returnM (maybe s f) ⟩ hunk ./CompositionBased/Exceptions.agda 205 - sub-cong s₁≈s₂ = λ x → Λ λ y → s₁≈s₂ (x ∸ y) + sub-cong s₁≈s₂ = λ x → Λ-cong λ y → s₁≈s₂ (x ∸ y) hunk ./CompositionBased/Exceptions.agda 208 - pop-cong f₁≈f₂ = Λ λ _ → f₁≈f₂ + pop-cong f₁≈f₂ = Λ-cong λ _ → f₁≈f₂ hunk ./CompositionBased/Exceptions.agda 245 - -- - -- (Except for a possible bug: At the time of writing Agda claims - -- that apply halt evaluates to Λ (_·_ (Λ λ x → return (just x))). hunk ./ReverseComposition.agda 25 -infixr 4 _⇨_ +-- Injection of values into the monad. + +record Done {ℓ} (A : Set ℓ) : Set ℓ where + constructor return + + -- Extraction of the result. + + field ! : A + +open Done public + +-- Abstraction. hunk ./ReverseComposition.agda 38 -data _⇨_ {ℓ} : List (Set ℓ) → Set ℓ → Set (suc ℓ) where - return : ∀ {B} (x : B) → [] ⇨ B - Λ : ∀ {A As B} (f : A → As ⇨ B) → (A ∷ As) ⇨ B +infixl 5 _→̂_ hunk ./ReverseComposition.agda 40 --- Application. +record _→̂_ {ℓ} (A B : Set ℓ) : Set ℓ where + constructor Λ hunk ./ReverseComposition.agda 43 -infixl 10 _·_ + -- Application. hunk ./ReverseComposition.agda 45 -_·_ : ∀ {ℓ} {A B : Set ℓ} {As} → (A ∷ As) ⇨ B → A → As ⇨ B -Λ f · x = f x + infixl 10 _·_ hunk ./ReverseComposition.agda 47 --- Extraction of the result. + field _·_ : A → B hunk ./ReverseComposition.agda 49 -! : ∀ {ℓ} {B : Set ℓ} → [] ⇨ B → B -! (return x) = x +open _→̂_ public + +-- Functions from a given number of arguments, with given types. + +infixr 4 _⇨_ + +_⇨_ : ∀ {ℓ} → List (Set ℓ) → Set ℓ → Set ℓ +[] ⇨ B = Done B +(A ∷ As) ⇨ B = A →̂ (As ⇨ B) hunk ./ReverseComposition.agda 66 - return : ∀ {B} {x₁ x₂ : B} → - (x₁≡x₂ : x₁ ≡ x₂) → return x₁ ≈ return x₂ - Λ : ∀ {A As₁ B₁ As₂ B₂} {f₁ : A → As₁ ⇨ B₁} {f₂ : A → As₂ ⇨ B₂} - (f₁≈f₂ : ∀ x → f₁ x ≈ f₂ x) → Λ f₁ ≈ Λ f₂ + return-cong : ∀ {B} {x₁ x₂ : B} → + (x₁≡x₂ : x₁ ≡ x₂) → return x₁ ≈ return x₂ + Λ-cong : ∀ {A As₁ B₁ As₂ B₂} + {f₁ : A → As₁ ⇨ B₁} {f₂ : A → As₂ ⇨ B₂} + (f₁≈f₂ : ∀ x → f₁ x ≈ f₂ x) → Λ f₁ ≈ Λ f₂ hunk ./ReverseComposition.agda 73 -refl (return x) = return P.refl -refl (Λ f) = Λ (λ x → refl (f x)) +refl {As = []} (return x) = return-cong P.refl +refl {As = A ∷ As} (Λ f) = Λ-cong (λ x → refl (f x)) hunk ./ReverseComposition.agda 78 -sym (return x≡y) = return (P.sym x≡y) -sym (Λ f≈g) = Λ (sym ∘ f≈g) +sym (return-cong x≡y) = return-cong (P.sym x≡y) +sym (Λ-cong f≈g) = Λ-cong (sym ∘ f≈g) hunk ./ReverseComposition.agda 84 -trans (return x≡y) (return y≡z) = return (P.trans x≡y y≡z) -trans (Λ f≈g) (Λ g≈h) = Λ (λ x → trans (f≈g x) (g≈h x)) +trans (return-cong x≡y) (return-cong y≡z) = + return-cong (P.trans x≡y y≡z) +trans (Λ-cong f≈g) (Λ-cong g≈h) = Λ-cong λ x → trans (f≈g x) (g≈h x) hunk ./ReverseComposition.agda 136 --- Eta equality. - -η : ∀ {ℓ As} {A B : Set ℓ} {f : (A ∷ As) ⇨ B} → Λ (λ x → f · x) ≡ f -η {f = Λ f} = P.refl - -η₀ : ∀ {ℓ} {A : Set ℓ} {x : [] ⇨ A} → return (! x) ≡ x -η₀ {x = return x} = P.refl - hunk ./ReverseComposition.agda 143 -Λ f₁≈f₂ ·-cong H.refl = f₁≈f₂ _ +Λ-cong f₁≈f₂ ·-cong H.refl = f₁≈f₂ _ hunk ./ReverseComposition.agda 147 -!-cong (return x₁≡x₂) = H.≡-to-≅ x₁≡x₂ +!-cong (return-cong x₁≡x₂) = H.≡-to-≅ x₁≡x₂ hunk ./ReverseComposition.agda 159 -return x >>= g = g x -Λ f >>= g = Λ λ x → f x >>= g +_>>=_ {As = []} x g = g (! x) +_>>=_ {As = A ∷ As} f g = Λ λ x → f · x >>= g hunk ./ReverseComposition.agda 172 - right-identity (return x) = refl (return x) - right-identity (Λ f) = Λ (λ x → right-identity (f x)) + right-identity {As = []} x = refl x + right-identity {As = A ∷ As} f = Λ-cong λ x → right-identity (f · x) hunk ./ReverseComposition.agda 178 - assoc (return x) g h = refl (g x >>= h) - assoc (Λ f) g h = Λ (λ x → assoc (f x) g h) + assoc {As = []} x g h = refl (g (! x) >>= h) + assoc {As = A ∷ As} f g h = Λ-cong λ x → assoc (f · x) g h hunk ./ReverseComposition.agda 188 - return x₁≡x₂ >>=-cong g₁≈g₂ = g₁≈g₂ (H.≡-to-≅ x₁≡x₂) - Λ f₁≈f₂ >>=-cong g₁≈g₂ = Λ λ x → f₁≈f₂ x >>=-cong g₁≈g₂ + return-cong x₁≡x₂ >>=-cong g₁≈g₂ = g₁≈g₂ (H.≡-to-≅ x₁≡x₂) + Λ-cong f₁≈f₂ >>=-cong g₁≈g₂ = Λ-cong λ x → f₁≈f₂ x >>=-cong g₁≈g₂ hunk ./ReverseComposition.agda 231 - (Λ λ x → f · x) ≡⟨ η ⟩ + (Λ λ x → f · x) ≡⟨ P.refl ⟩ hunk ./ReverseComposition.agda 239 - assoc f (Λ g) h = - (f ⊙ Λ g) ⊙ h ≡⟨ P.refl ⟩ - f >>= g >>= _·_ h ≈⟨ MonadLaws.assoc f g (_·_ h) ⟩ - f >>= (λ x → g x >>= _·_ h) ≈⟨ refl f >>=-cong (λ x₁≅x₂ → - (refl (Λ g) ·-cong x₁≅x₂) >>=-cong - _·-cong_ (refl h)) ⟩ - f ⊙ (Λ g ⊙ h) ∎ + assoc f g h = + (f ⊙ g) ⊙ h ≡⟨ P.refl ⟩ + f >>= _·_ g >>= _·_ h ≈⟨ MonadLaws.assoc f (_·_ g) (_·_ h) ⟩ + f >>= (λ x → g · x >>= _·_ h) ≈⟨ refl f >>=-cong (λ x₁≅x₂ → + (refl g ·-cong x₁≅x₂) >>=-cong + _·-cong_ (refl h)) ⟩ + f ⊙ (g ⊙ h) ∎ hunk ./ReverseComposition.agda 265 -uncurry (return x) _ = x -uncurry (Λ f) (a , as) = uncurry (f a) as +uncurry {As = []} x _ = ! x +uncurry {As = A ∷ As} f (a , as) = uncurry (f · a) as hunk ./ReverseComposition.agda 276 - curry∘uncurry (return x) = return P.refl - curry∘uncurry (Λ f) = Λ λ a → curry∘uncurry (f a) + curry∘uncurry {As = []} x = return-cong P.refl + curry∘uncurry {As = A ∷ As} f = Λ-cong λ a → curry∘uncurry (f · a) hunk ./ReverseComposition.agda 286 - curry-cong {[]} f₁≗f₂ = return (f₁≗f₂ _) - curry-cong {A ∷ As} f₁≗f₂ = Λ λ a → curry-cong (λ as → f₁≗f₂ (a , as)) + curry-cong {[]} f₁≗f₂ = return-cong (f₁≗f₂ _) + curry-cong {A ∷ As} f₁≗f₂ = Λ-cong λ a → + curry-cong (λ as → f₁≗f₂ (a , as)) hunk ./ReverseComposition.agda 292 - uncurry-cong (return x₁≡x₂) _ = x₁≡x₂ - uncurry-cong (Λ f₁≈f₂) (a , as) = uncurry-cong (f₁≈f₂ a) as + uncurry-cong (return-cong x₁≡x₂) _ = x₁≡x₂ + uncurry-cong (Λ-cong f₁≈f₂) (a , as) = uncurry-cong (f₁≈f₂ a) as hunk ./ReverseComposition.agda 300 -_↑_⇨_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ → Set (suc ℓ) +_↑_⇨_ : ∀ {ℓ} → Set ℓ → ℕ → Set ℓ → Set ℓ hunk ./ReverseComposition.agda 323 -return x >>=∥ g = g x -Λ f >>=∥ g = Λ λ x → f x >>=∥ λ y → g y · x +f >>=∥ g = curry λ as → uncurry (g (uncurry f as)) as hunk ./ReverseComposition.agda 335 - Λ (λ y → return∥ x >>=∥ λ z → f z · y) ≈⟨ Λ (λ y → left-identity (λ z → f z · y) x) ⟩ - Λ (λ y → f x · y) ≡⟨ η ⟩ + Λ (λ y → return∥ x >>=∥ λ z → f z · y) ≈⟨ Λ-cong (λ y → left-identity (λ z → f z · y) x) ⟩ + Λ (λ y → f x · y) ≡⟨ P.refl ⟩ hunk ./ReverseComposition.agda 341 - right-identity (return x) = refl (return x) - right-identity (Λ f) = Λ λ x → right-identity (f x) + right-identity {As = []} x = refl x + right-identity {As = _ ∷ _} f = Λ-cong λ x → right-identity (f · x) hunk ./ReverseComposition.agda 346 - return∥-cong {As = []} x₁≡x₂ = return x₁≡x₂ - return∥-cong {As = A ∷ As} x₁≡x₂ = Λ λ _ → return∥-cong x₁≡x₂ + return∥-cong {As = []} x₁≡x₂ = return-cong x₁≡x₂ + return∥-cong {As = A ∷ As} x₁≡x₂ = Λ-cong λ _ → return∥-cong x₁≡x₂ hunk ./ReverseComposition.agda 356 - return x₁≡x₂ >>=∥-cong g₁≈g₂ = g₁≈g₂ (H.≡-to-≅ x₁≡x₂) - Λ f₁≈f₂ >>=∥-cong g₁≈g₂ = Λ λ x → + return-cong x₁≡x₂ >>=∥-cong g₁≈g₂ = g₁≈g₂ (H.≡-to-≅ x₁≡x₂) + Λ-cong f₁≈f₂ >>=∥-cong g₁≈g₂ = Λ-cong λ x → hunk ./ReverseComposition.agda 369 - private - - unfold : ∀ {As} {A B C : Set ℓ} {x} - (f : A ∷ As ⇨ B) (g : B → A ∷ As ⇨ C) → - (f >>=∥ g) · x ≈ f · x >>=∥ (λ y → g y · x) - unfold (Λ f) g = refl _ - hunk ./ReverseComposition.agda 372 - assoc (return x) g h = refl (g x >>=∥ h) - assoc (Λ f) g h = Λ λ x → - (f x >>=∥ λ y → g y · x) >>=∥ (λ y → h y · x) ≈⟨ assoc (f x) (λ y → g y · x) (λ y → h y · x) ⟩ - f x >>=∥ (λ y → g y · x >>=∥ λ z → h z · x) ≈⟨ (refl (f x) >>=∥-cong λ {y₁ y₂} y₁≅y₂ → - - g y₁ · x >>=∥ (λ z → h z · x) ≈⟨ sym $ unfold (g y₁) h ⟩ - (g y₁ >>=∥ h) · x ≡⟨ P.cong (λ y → (g y >>=∥ h) · x) (H.≅-to-≡ y₁≅y₂) ⟩ - (g y₂ >>=∥ h) · x ∎) ⟩ - - f x >>=∥ (λ y → (g y >>=∥ h) · x) ∎ + assoc {As = []} x g h = refl (g (! x) >>=∥ h) + assoc {As = _ ∷ _} f g h = Λ-cong λ x → + (f · x >>=∥ λ y → g y · x) >>=∥ (λ y → h y · x) ≈⟨ assoc (f · x) (λ y → g y · x) (λ y → h y · x) ⟩ + f · x >>=∥ (λ y → g y · x >>=∥ λ z → h z · x) ≡⟨ P.refl ⟩ + f · x >>=∥ (λ y → (g y >>=∥ h) · x) ∎ hunk ./ReverseComposition.agda 404 - return∥->>= (A ∷ As) x f = Λ λ _ → return∥->>= As x f + return∥->>= (A ∷ As) x f = Λ-cong λ _ → return∥->>= As x f hunk ./ReverseComposition.agda 409 - >>=-return∥ (return x) y = refl (return∥ y) - >>=-return∥ (Λ f) y = Λ λ x → >>=-return∥ (f x) y + >>=-return∥ {As = []} x y = refl (return∥ y) + >>=-return∥ {As = _ ∷ _} f y = Λ-cong λ x → >>=-return∥ (f · x) y hunk ./ReverseComposition.agda 422 - map-∘ f g h = - (h >>=∥ return∥ ∘ g) >>=∥ return∥ ∘ f ≈⟨ assoc h _ _ ⟩ - h >>=∥ (λ x → return∥ (g x) >>=∥ return∥ ∘ f) ≈⟨ (refl h >>=∥-cong′ λ x → left-identity _ _) ⟩ + map-∘ {As = As} f g h = + (h >>=∥ return∥ ∘ g) >>=∥ return∥ ∘ f ≈⟨ assoc h (return∥ ∘ g) (return∥ ∘ f) ⟩ + h >>=∥ (λ x → return∥ (g x) >>=∥ return∥ ∘ f) ≈⟨ (refl h >>=∥-cong′ λ x → left-identity (return∥ {As = As} ∘ f) (g x)) ⟩ hunk ./ReverseComposition.agda 433 - map-⊙ f (return x) (Λ h) = - map f (return x ⊙ Λ h) ≡⟨ P.refl ⟩ - map f (h x) ≡⟨ P.refl ⟩ - return x ⊙ map f (Λ h) ∎ - map-⊙ f (Λ g) h = - map f (Λ g ⊙ h) ≡⟨ P.refl ⟩ - (Λ λ x → g x ⊙ h >>=∥ λ y → return∥ (f y) · x) ≈⟨ (Λ λ x → refl (g x ⊙ h) >>=∥-cong′ λ y → refl (return∥ (f y))) ⟩ - (Λ λ x → g x ⊙ h >>=∥ return∥ ∘ f) ≡⟨ P.refl ⟩ - (Λ λ x → map f (g x ⊙ h)) ≈⟨ (Λ λ x → map-⊙ f (g x) h) ⟩ - (Λ λ x → g x ⊙ map f h) ≡⟨ P.refl ⟩ - Λ g ⊙ map f h ∎ + map-⊙ {As = []} f x h = + map f (x ⊙ h) ≡⟨ P.refl ⟩ + map f (h · ! x) ≡⟨ P.refl ⟩ + x ⊙ map f h ∎ + map-⊙ {As = _ ∷ _} f g h = + map f (g ⊙ h) ≡⟨ P.refl ⟩ + (Λ λ x → g · x ⊙ h >>=∥ λ y → return∥ (f y) · x) ≈⟨ (Λ-cong λ x → refl (g · x ⊙ h) >>=∥-cong′ λ y → refl (return∥ (f y))) ⟩ + (Λ λ x → g · x ⊙ h >>=∥ return∥ ∘ f) ≡⟨ P.refl ⟩ + (Λ λ x → map f (g · x ⊙ h)) ≈⟨ (Λ-cong λ x → map-⊙ f (g · x) h) ⟩ + (Λ λ x → g · x ⊙ map f h) ≡⟨ P.refl ⟩ + g ⊙ map f h ∎ hunk ./ReverseComposition.agda 449 - left-identity f x ys = - (return∥ f >>=∥ λ h → return∥ x >>=∥ return∥ ∘ h) >>=∥ (λ h → map h ys) ≈⟨ (MonadLaws∥.left-identity _ _ >>=∥-cong′ λ _ → refl _) ⟩ - (return∥ x >>=∥ return∥ ∘ f) >>=∥ (λ h → map h ys) ≈⟨ (MonadLaws∥.left-identity _ _ >>=∥-cong′ λ _ → refl _) ⟩ - return∥ (f x) >>=∥ (λ h → map h ys) ≈⟨ MonadLaws∥.left-identity _ _ ⟩ + left-identity {As = As} f x ys = + (return∥ f >>=∥ λ h → return∥ x >>=∥ return∥ ∘ h) >>=∥ (λ h → map h ys) ≈⟨ (MonadLaws∥.left-identity + (λ h → return∥ x >>=∥ return∥ ∘ h) f >>=∥-cong′ λ h → + refl (map h ys)) ⟩ + (return∥ x >>=∥ return∥ ∘ f) >>=∥ (λ h → map h ys) ≈⟨ (MonadLaws∥.left-identity + (return∥ {As = As} ∘ f) x >>=∥-cong′ λ h → + refl (map h ys)) ⟩ + return∥ (f x) >>=∥ (λ h → map h ys) ≈⟨ MonadLaws∥.left-identity (λ h → map h ys) (f x) ⟩ hunk ./ReverseComposition.agda 463 - right-identity f xs y = - (return∥ f >>=∥ λ h → map h xs) >>=∥ (λ h → return∥ y >>=∥ return∥ ∘ h) ≈⟨ (MonadLaws∥.left-identity _ _ >>=∥-cong′ λ _ → - MonadLaws∥.left-identity _ _) ⟩ + right-identity {As = As} f xs y = + (return∥ f >>=∥ λ h → map h xs) >>=∥ (λ h → return∥ y >>=∥ return∥ ∘ h) ≈⟨ (MonadLaws∥.left-identity (λ h → map h xs) f + >>=∥-cong′ λ h → + MonadLaws∥.left-identity (return∥ {As = As} ∘ h) y) ⟩ hunk ./ReverseComposition.agda 468 - (xs >>=∥ return∥ ∘ f) >>=∥ (λ h → return∥ (h y)) ≈⟨ assoc xs _ _ ⟩ - xs >>=∥ (λ x → return∥ (f x) >>=∥ λ h → return∥ (h y)) ≈⟨ (refl xs >>=∥-cong′ λ _ → MonadLaws∥.left-identity _ _) ⟩ + (xs >>=∥ return∥ ∘ f) >>=∥ (λ h → return∥ (h y)) ≈⟨ assoc xs (return∥ ∘ f) (λ h → return∥ (h y)) ⟩ + xs >>=∥ (λ x → return∥ (f x) >>=∥ λ h → return∥ (h y)) ≈⟨ (refl xs >>=∥-cong′ λ x → + MonadLaws∥.left-identity (λ h → return∥ (h y)) (f x)) ⟩ hunk ./ReverseComposition.agda 481 - assoc (return x) (return y) (return z) hyp = return (hyp x y z) - assoc (Λ f) (Λ g) (Λ h) hyp = - Λ λ x → assoc (f x) (g x) (h x) hyp + assoc {As = []} x y z hyp = return-cong (hyp (! x) (! y) (! z)) + assoc {As = _ ∷ _} f g h hyp = + Λ-cong λ x → assoc (f · x) (g · x) (h · x) hyp hunk ./ReverseComposition.agda 504 - zipWith∥-cong f₁≡f₂ (return P.refl) (return P.refl) = - return (f₁≡f₂ _ _) - zipWith∥-cong f₁≡f₂ (Λ g₁≈g₂) (Λ h₁≈h₂) = Λ λ x → - zipWith∥-cong f₁≡f₂ (g₁≈g₂ x) (h₁≈h₂ x) - - -- _>>=∥_ can be defined using curry and uncurry. - - >>=∥-curry-uncurry : - ∀ {As} {B C : Set ℓ} (f : As ⇨ B) (g : B → As ⇨ C) → - f >>=∥ g ≈ curry {As = As} (λ as → uncurry (g (uncurry f as)) as) - >>=∥-curry-uncurry (return x) g with g x - ... | return y = - return y ≡⟨ P.refl ⟩ - return (uncurry (return y) _) ∎ - >>=∥-curry-uncurry (Λ {As = As} f) g = Λ λ a → - let h = λ (as : Args As) → g (uncurry (f a) as) in - (f a >>=∥ λ y → g y · a) ≈⟨ >>=∥-curry-uncurry (f a) (λ y → g y · a) ⟩ - curry (λ as → uncurry (h as · a) as) ≡⟨ P.refl ⟩ - curry (λ as → uncurry (Λ λ x → h as · x) (a , as)) ≈⟨ curry-cong (λ as → uncurry-cong (complete (η {f = h as})) (a , as)) ⟩ - curry (λ as → uncurry (h as) (a , as)) ∎ - where open CurryLaws + zipWith∥-cong f₁≡f₂ (return-cong P.refl) (return-cong P.refl) = + return-cong (f₁≡f₂ _ _) + zipWith∥-cong f₁≡f₂ (Λ-cong g₁≈g₂) (Λ-cong h₁≈h₂) = + Λ-cong λ x → zipWith∥-cong f₁≡f₂ (g₁≈g₂ x) (h₁≈h₂ x) hunk ./ReverseComposition.agda 515 - (f >>=∥ λ h → g >>=∥ λ x → return∥ (h x)) ≈⟨ >>=∥-curry-uncurry f _ ⟩ - curry (λ as → uncurry (g >>=∥ λ x → return∥ (uncurry f as x)) as) ≈⟨ curry-cong (λ as → - uncurry-cong {As = As} - (>>=∥-curry-uncurry g (return∥ ∘ uncurry f as)) - as) ⟩ + (f >>=∥ λ h → g >>=∥ λ x → return∥ (h x)) ≡⟨ P.refl ⟩ hunk ./ReverseComposition.agda 539 -_⇨M_ : ∀ {ℓ} → List (Set ℓ) → Set ℓ → Set (suc ℓ) +_⇨M_ : ∀ {ℓ} → List (Set ℓ) → Set ℓ → Set ℓ hunk ./ReverseComposition.agda 580 - maybe-cong : ∀ {Bs₁ Bs₂} {B C₁ C₂ : Set ℓ} + maybe′-cong : ∀ {Bs₁ Bs₂} {B C₁ C₂ : Set ℓ} hunk ./ReverseComposition.agda 584 - ∀ x → maybe s₁ f₁ x ≈ maybe s₂ f₂ x - maybe-cong s₁≈s₂ f₁≈f₂ (just x) = s₁≈s₂ x - maybe-cong s₁≈s₂ f₁≈f₂ nothing = f₁≈f₂ + ∀ x → maybe′ s₁ f₁ x ≈ maybe′ s₂ f₂ x + maybe′-cong s₁≈s₂ f₁≈f₂ (just x) = s₁≈s₂ x + maybe′-cong s₁≈s₂ f₁≈f₂ nothing = f₁≈f₂ hunk ./ReverseComposition.agda 596 - g₁≈g₂ >>=-cong′ maybe-cong s₁≈s₂ f₁≈f₂ + g₁≈g₂ >>=-cong′ maybe′-cong s₁≈s₂ f₁≈f₂ hunk ./ReverseComposition.agda 632 - {h : Maybe C → Cs ⇨M D} → + (h : Maybe C → Cs ⇨M D) → hunk ./ReverseComposition.agda 635 - distrib g s {f} {h} = + distrib g s {f} h = hunk ./ReverseComposition.agda 720 - (Λ λ x → f · x) ≡⟨ η ⟩ + (Λ λ x → f · x) ≡⟨ P.refl ⟩