From 258821e9d6ed9a1e99326431f4511d457fcc9514 Mon Sep 17 00:00:00 2001
From: anuyts <anuyts@users.noreply.github.com>
Date: Tue, 3 May 2022 15:34:59 +0200
Subject: [PATCH] Contravariance of categories of algebras (#767)

* Define IsMonad.

* HomFunctor.

* bind as a natural transformation.

* Functor algebras (WIP).

* Functor algebras.

* Eilenberg-Moore category.

* Variance of category of algebras.

* No eta-equality for Category.

* Shorten long lines.

* Reenable eta-equality for categories.

* Uncomment involutiveOp.
---
 .../Categories/Instances/FunctorAlgebras.agda | 27 +++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/Cubical/Categories/Instances/FunctorAlgebras.agda b/Cubical/Categories/Instances/FunctorAlgebras.agda
index 6a25ddae7c..be02f448b4 100644
--- a/Cubical/Categories/Instances/FunctorAlgebras.agda
+++ b/Cubical/Categories/Instances/FunctorAlgebras.agda
@@ -9,6 +9,7 @@ open import Cubical.Foundations.Univalence
 
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
+open import Cubical.Categories.NaturalTransformation.Base
 
 open _≅_
 
@@ -106,3 +107,29 @@ module _ {C : Category ℓC ℓC'} (F : Functor C C) where
   F-hom ForgetAlgebra = carrierHom
   F-id ForgetAlgebra = refl
   F-seq ForgetAlgebra algF algG = refl
+
+module _ {C : Category ℓC ℓC'} {F G : Functor C C} (τ : NatTrans F G) where
+
+  private
+    module C = Category C
+  open Functor
+  open NatTrans
+  open AlgebraHom
+
+  AlgebrasFunctor : Functor (AlgebrasCategory G) (AlgebrasCategory F)
+  F-ob AlgebrasFunctor (algebra a α) = algebra a (α C.∘ N-ob τ a)
+  carrierHom (F-hom AlgebrasFunctor (algebraHom f isalgF)) = f
+  strHom (F-hom AlgebrasFunctor {algebra a α} {algebra b β} (algebraHom f isalgF)) =
+    (N-ob τ a C.⋆ α) C.⋆ f
+      ≡⟨ C.⋆Assoc (N-ob τ a) α f ⟩
+    N-ob τ a C.⋆ (α C.⋆ f)
+      ≡⟨ cong (N-ob τ a C.⋆_) isalgF ⟩
+    N-ob τ a C.⋆ (F-hom G f C.⋆ β)
+      ≡⟨ sym (C.⋆Assoc _ _ _) ⟩
+    (N-ob τ a C.⋆ F-hom G f) C.⋆ β
+      ≡⟨ cong (C._⋆ β) (sym (N-hom τ f)) ⟩
+    (F-hom F f C.⋆ N-ob τ b) C.⋆ β
+      ≡⟨ C.⋆Assoc _ _ _ ⟩
+    F-hom F f C.⋆ (N-ob τ b C.⋆ β) ∎
+  F-id AlgebrasFunctor = AlgebraHom≡ F refl
+  F-seq AlgebrasFunctor algΦ algΨ = AlgebraHom≡ F refl