module Cubical.Categories.Profunctor.Homomorphism.Unary where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure
open import Cubical.Data.Sigma
open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Functors
open import Cubical.Categories.Profunctor.Relator hiding (natL; natR)

private
  variable
    ℓB ℓB' ℓC ℓC' ℓD ℓD' ℓS ℓR ℓQ : Level

module _ {C : Category ℓC ℓC'}
         {D : Category ℓD ℓD'} where
  -- this is "just" a natural transformation, should we take advantage of that?
  record Homomorphism (R : C o-[ ℓR ]-* D)
                      (S : C o-[ ℓS ]-* D)
         : Type (ℓ-max (ℓ-max ℓC ℓC')
                (ℓ-max (ℓ-max ℓD ℓD')
                (ℓ-max ℓR ℓS))) where
    field
      hom : ∀ {c d} → R [ c , d ]R → S [ c , d ]R
      natL : ∀ {c' c d} (f : C [ c , c' ]) (r : R [ c' , d ]R)
           → hom (f ⋆l⟨ R ⟩ r ) ≡ f ⋆l⟨ S ⟩ hom r
      natR : ∀ {c d d'} (r : R [ c , d ]R) (h : D [ d , d' ])
           → hom (r ⋆r⟨ R ⟩ h) ≡ hom r ⋆r⟨ S ⟩ h

  open Homomorphism

  isIsoH : ∀ {R : C o-[ ℓR ]-* D} {S : C o-[ ℓS ]-* D}
        → Homomorphism R S → Type _
  isIsoH h = ∀ {c d} → isEquiv (h .hom {c}{d})