{-# OPTIONS --without-K --safe #-}

-- Some properties of 'heterogeneous' identity morphisms

module Categories.Morphism.HeterogeneousIdentity.Properties where

open import Level
open import Data.Product using (curry) renaming (_,_ to _,,_)
open import Relation.Binary.PropositionalEquality

open import Categories.Category using (Category; _[_,_]; _[_≈_])
open import Categories.Category.Product
open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Functor.Bifunctor
open import Categories.Morphism.HeterogeneousIdentity

private
  variable
    o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ : Level

open Category using (Obj; id)

-- Functor identity laws lifted to heterogeneous identities.

hid-identity : (C : Category o ℓ e) (D : Category o′ ℓ′ e′)
               {F₀ : Obj C → Obj D}
               (F₁ : ∀ {A B} → C [ A , B ] → D [ F₀ A , F₀ B ]) →
               (∀ {A} → D [ F₁ (id C {A}) ≈ id D ]) →
               ∀ {A B} (p : A ≡ B) → D [ F₁ (hid C p) ≈ hid D (cong F₀ p) ]
hid-identity C D F₁ hyp refl = hyp

hid-identity₂ : (C₁ : Category o ℓ e) (C₂ : Category o′ ℓ′ e′)
                (D : Category o″ ℓ″ e″)
                {F₀ : Obj C₁ → Obj C₂ → Obj D}
                (F₁ : ∀ {A₁ A₂ B₁ B₂} → C₁ [ A₁ , B₁ ] → C₂ [ A₂ , B₂ ] →
                      D [ F₀ A₁ A₂ , F₀ B₁ B₂ ]) →
                (∀ {A₁ A₂} → D [ F₁ (id C₁ {A₁}) (id C₂ {A₂}) ≈ id D ]) →
                ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
                D [ F₁ (hid C₁ p) (hid C₂ q) ≈ hid D (cong₂ F₀ p q) ]
hid-identity₂ C₁ C₂ D F₁ hyp refl refl = hyp

module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′}
         (F : Functor C D) where
  open Category D
  open Functor F

  -- functors preserve heterogeneous identities

  F-hid : ∀ {A B} (p : A ≡ B) → F₁ (hid C p) ≈ hid D (cong F₀ p)
  F-hid = hid-identity C D F₁ identity

module _ {C₁ : Category o ℓ e} {C₂ : Category o′ ℓ′ e′}
         {D : Category o″ ℓ″ e″} (F : Bifunctor C₁ C₂ D) where
  open Category D
  open Functor F

  -- bifunctors preserve heterogeneous identities

  BF-hid : ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
           F₁ (hid C₁ p ,, hid C₂ q) ≈ hid D (cong₂ (curry F₀) p q)
  BF-hid = hid-identity₂ C₁ C₂ D (curry F₁) identity

module _ (C : Category o ℓ e) (D : Category o′ ℓ′ e′) where
  open Category (Product C D)

  -- products preserve heterogeneous identities

  ×-hid : ∀ {A₁ A₂ B₁ B₂} (p : A₁ ≡ B₁) (q : A₂ ≡ B₂) →
          (hid C p ,, hid D q) ≈ hid (Product C D) (cong₂ _,,_ p q)
  ×-hid p q = BF-hid {C₁ = C} {C₂ = D} (idF ⁂ idF) p q