From 9ec6ce9eba01ca646eee85144ef35f357cd4afb9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 5 Mar 2018 17:10:41 +0100
Subject: [PATCH] Use other equality principle

---
 src/Cat/Categories/Cat.agda   | 16 +++++-----------
 src/Cat/Category/Functor.agda | 19 ++-----------------
 src/Cat/Category/Monad.agda   | 20 ++++++++++++--------
 3 files changed, 19 insertions(+), 36 deletions(-)

diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda
index 2bed7c2..ce493b6 100644
--- a/src/Cat/Categories/Cat.agda
+++ b/src/Cat/Categories/Cat.agda
@@ -25,14 +25,14 @@ module _ (ℓ ℓ' : Level) where
   private
     module _ {𝔸 𝔹 ℂ 𝔻 : Category ℓ ℓ'} {F : Functor 𝔸 𝔹} {G : Functor 𝔹 ℂ} {H : Functor ℂ 𝔻} where
       assc : F[ H ∘ F[ G ∘ F ] ] ≡ F[ F[ H ∘ G ] ∘ F ]
-      assc = Functor≡ refl refl
+      assc = Functor≡ refl
 
     module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where
       ident-r : F[ F ∘ identity ] ≡ F
-      ident-r = Functor≡ refl refl
+      ident-r = Functor≡ refl
 
       ident-l : F[ identity ∘ F ] ≡ F
-      ident-l = Functor≡ refl refl
+      ident-l = Functor≡ refl
 
   RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ')
   RawCat =
@@ -133,16 +133,10 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where
           open module x₂ = Functor x₂
 
       isUniqL : F[ proj₁ ∘ x ] ≡ x₁
-      isUniqL = Functor≡ eq* eq→
-        where
-          eq* : (F[ proj₁ ∘ x ]) .func* ≡ x₁ .func*
-          eq* = refl
-          eq→ : (λ i → {A : Object X} {B : Object X} → X [ A , B ] → ℂ [ eq* i A , eq* i B ])
-                  [ (F[ proj₁ ∘ x ]) .func→ ≡ x₁ .func→ ]
-          eq→ = refl
+      isUniqL = Functor≡ refl
 
       isUniqR : F[ proj₂ ∘ x ] ≡ x₂
-      isUniqR = Functor≡ refl refl
+      isUniqR = Functor≡ refl
 
       isUniq : F[ proj₁ ∘ x ] ≡ x₁ × F[ proj₂ ∘ x ] ≡ x₂
       isUniq = isUniqL , isUniqR
diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index 08400ea..e9a28fc 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -112,25 +112,10 @@ module _
 
 module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where
   Functor≡ : {F G : Functor ℂ 𝔻}
-    → (eq* : func* F ≡ func* G)
-    → (eq→ : (λ i → ∀ {x y} → ℂ [ x , y ] → 𝔻 [ eq* i x , eq* i y ])
-        [ func→ F ≡ func→ G ])
-    → F ≡ G
-  Functor≡ {F} {G} eq* eq→ i = record
-    { raw = eqR i
-    ; isFunctor = eqIsF i
-    }
-    where
-      eqR : raw F ≡ raw G
-      eqR i = record { func* = eq* i ; func→ = eq→ i }
-      eqIsF : (λ i →  IsFunctor ℂ 𝔻 (eqR i)) [ isFunctor F ≡ isFunctor G ]
-      eqIsF = IsFunctorIsProp' (isFunctor F) (isFunctor G)
-
-  FunctorEq : {F G : Functor ℂ 𝔻}
     → raw F ≡ raw G
     → F ≡ G
-  raw (FunctorEq eq i) = eq i
-  isFunctor (FunctorEq {F} {G} eq i)
+  raw       (Functor≡ eq i) = eq i
+  isFunctor (Functor≡ {F} {G} eq i)
     = res i
     where
     res : (λ i →  IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ]
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 8ba97df..151d27c 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -6,7 +6,7 @@ open import Agda.Primitive
 open import Data.Product
 
 open import Cubical
-open import Cubical.NType.Properties using (lemPropF)
+open import Cubical.NType.Properties using (lemPropF ; lemSig)
 
 open import Cat.Category
 open import Cat.Category.Functor as F
@@ -537,8 +537,12 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       rawEq→ : P (RawFunctor.func* right) refl (RawFunctor.func→ right)
       -- rawEq→ : (fmap' : Fmap ℂ ℂ {!!}) → RawFunctor.func→ left ≡ fmap'
       rawEq→ = begin
-        (λ {A} {B} → RawFunctor.func→ left) ≡⟨ {!!} ⟩
-        (λ {A} {B} → RawFunctor.func→ right) ∎
+        (λ f → RawFunctor.func→ left f) ≡⟨⟩
+        (λ f → KM.fmap f)               ≡⟨⟩
+        (λ f → KM.bind (f >>> KM.pure)) ≡⟨ {!!} ⟩
+        (λ f → RawFunctor.func→ right f) ∎
+        where
+        module KM = K.Monad (forth m)
       -- destfmap =
       source = (Functor.raw (K.Monad.R (forth m)))
       -- p : (fmap' : Fmap ℂ ℂ (RawFunctor.func* source)) → (λ i → Fmap ℂ ℂ (refl i)) [ func→ source ≡ fmap' ]
@@ -546,16 +550,16 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       rawEq : Functor.raw (K.Monad.R (forth m)) ≡ Functor.raw R
       rawEq = RawFunctor≡ ℂ ℂ {x = left} {right} refl λ fmap'  → {!rawEq→!}
       Req : M.RawMonad.R (backRaw (forth m)) ≡ R
-      Req = FunctorEq rawEq
+      Req = Functor≡ rawEq
 
-      ηeq : M.RawMonad.η (backRaw (forth m)) ≡ η
-      ηeq = {!!}
-      postulate ηNatTransEq : {!!} [ M.RawMonad.ηNatTrans (backRaw (forth m)) ≡ ηNatTrans ]
       open NaturalTransformation ℂ ℂ
+      postulate
+        ηNatTransEq : (λ i → NaturalTransformation F.identity (Req i))
+          [ M.RawMonad.ηNatTrans (backRaw (forth m)) ≡ ηNatTrans ]
       backRawEq : backRaw (forth m) ≡ M.Monad.raw m
       -- stuck
       M.RawMonad.R         (backRawEq i) = Req i
-      M.RawMonad.ηNatTrans (backRawEq i) = let t = NaturalTransformation≡ F.identity R ηeq in {!t i!}
+      M.RawMonad.ηNatTrans (backRawEq i) = {!!} -- ηNatTransEq i
       M.RawMonad.μNatTrans (backRawEq i) = {!!}
 
     backeq : (m : M.Monad) → back (forth m) ≡ m