From 93d075a6d31d3a7434a4e4294d05f6f55c150fa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Wed, 7 Mar 2018 15:23:07 +0100
Subject: [PATCH] Attempt at proving `pureNTEq`

---
 src/Cat/Category/Functor.agda |  1 +
 src/Cat/Category/Monad.agda   | 58 ++++++++++++++++++++++++++++++++---
 2 files changed, 54 insertions(+), 5 deletions(-)

diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda
index e9a28fc..d627539 100644
--- a/src/Cat/Category/Functor.agda
+++ b/src/Cat/Category/Functor.agda
@@ -61,6 +61,7 @@ module _ {ℓc ℓc' ℓd ℓd'}
   record IsFunctor (F : RawFunctor) : 𝓤 where
     open RawFunctor F public
     field
+      -- TODO Really ought to be preserves identity or something like this.
       isIdentity : IsIdentity
       isDistributive : IsDistributive
 
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 7ffe664..279e457 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -534,13 +534,61 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where
       Req = Functor≡ rawEq
 
       open NaturalTransformation ℂ ℂ
-      postulate
-        pureNTEq : (λ i → NaturalTransformation F.identity (Req i))
+
+      pureTEq : M.RawMonad.pureT (backRaw (forth m)) ≡ pureT
+      pureTEq = funExt (λ X → refl)
+
+      -- TODO: Make equaility principle for natural transformations that allows
+      -- us to only focus on the data-part but for heterogeneous paths!
+      --
+      -- It should be something like (but not exactly because this is ill-typed!)
+      --
+      -- P : I → Set -- A family that varies over natural transformations.
+      -- θ : P i0
+      -- η : P i1
+      NaturalTransformation~≡ : ∀ {F G} {P : I → Set _} {θ η : NaturalTransformation F G} → proj₁ θ ≡ proj₁ η → _ [ θ ≡ η ]
+      NaturalTransformation~≡ = {!!}
+
+      pureNTEq : (λ i → NaturalTransformation F.identity (Req i))
+        [ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
+      pureNTEq = res
+        where
+        Base = Transformation F.identity R
+        base : Base
+        base = M.RawMonad.pureT (backRaw (forth m))
+        target : Base
+        target = pureT
+        -- No matter what the proof of naturality is (whether it'd be at `base`
+        -- or at `target` propositionality of naturality means that we can prove
+        -- two natural transformations equal just by focusing on the data-part.
+        d : {nat : Natural F.identity R base}
+          → (λ i → NaturalTransformation F.identity R)
+          [ (base   , nat)
+          ≡ (target , nat)
+          ]
+        d = NaturalTransformation≡ F.identity R pureTEq
+        -- I think that `d` should be the "base-case" somehow in my
+        -- path-induction but I don't know how to define a suitable type-family.
+        D : (y : Base) → ({!!} ≡ y) → Set _
+        D y eq = {!!}
+        res
+          : (λ i → NaturalTransformation F.identity (Req i))
           [ M.RawMonad.pureNT (backRaw (forth m)) ≡ pureNT ]
-        joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))
-          [ M.RawMonad.joinNT (backRaw (forth m)) ≡ joinNT ]
+        res = pathJ D d base pureTEq {!!}
+
+      joinTEq : M.RawMonad.joinT (backRaw (forth m)) ≡ joinT
+      joinTEq = funExt (λ X → begin
+        M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩
+        KM.join ≡⟨⟩
+        joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩
+        joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩
+        joinT X ∎)
+
+      joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i))
+        [ M.RawMonad.joinNT (backRaw (forth m)) ≡ joinNT ]
+      joinNTEq = NaturalTransformation~≡ joinTEq
+
       backRawEq : backRaw (forth m) ≡ M.Monad.raw m
-      -- stuck
       M.RawMonad.R      (backRawEq i) = Req i
       M.RawMonad.pureNT (backRawEq i) = pureNTEq i
       M.RawMonad.joinNT (backRawEq i) = joinNTEq i