invariant-imap-iso-is-iso.agda

{-# OPTIONS --cubical --safe #-}

open import Agda.Primitive
  renaming (Set to Type ; Setω to Typeω)
  hiding (Prop)
  public

open import Agda.Primitive.Cubical
  renaming (primTransp to transp ; primHComp to hcomp ; primINeg to ~_)
open import Agda.Builtin.Cubical.Path

Path : ∀ {ℓ} (A : Type ℓ) → A → A → Type ℓ
Path A = PathP (λ i → A)

private
  to-path : ∀ {ℓ} {A : Type ℓ} → (f : I → A) → Path A (f i0) (f i1)
  to-path f i = f i

_∙∙_∙∙_ : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
        → w ≡ x → x ≡ y → y ≡ z
        → w ≡ z
(p ∙∙ q ∙∙ r) i =
  hcomp (λ j → λ { (i = i0) → p (~ j)
                 ; (i = i1) → r j })
        (q i)

refl : ∀ {ℓ} {A : Type ℓ} {x : A} → x ≡ x
refl {x = x} = to-path (λ i → x)

sym : ∀ {ℓ} {A : Type ℓ} {x y : A}
    → x ≡ y → y ≡ x
sym p i = p (~ i)

_∙_ : ∀ {ℓ} {A : Type ℓ} {x y z : A}
    → x ≡ y → y ≡ z → x ≡ z
p ∙ q = refl ∙∙ p ∙∙ q

ap : ∀ {a b} {A : Type a} {B : A → Type b} (f : (x : A) → B x) {x y : A}
   → (p : x ≡ y) → PathP (λ i → B (p i)) (f x) (f y)
ap f p i = f (p i)

≡〈〉-syntax : ∀ {ℓ} {A : Type ℓ} (x : A) {y z} → y ≡ z → x ≡ y → x ≡ z
≡〈〉-syntax x q p = p ∙ q

infixr 2 ≡〈〉-syntax
syntax ≡〈〉-syntax x q p = x ≡〈 p 〉 q

_≡˘〈_〉_ : ∀ {ℓ} {A : Type ℓ} (x : A) {y z : A} → y ≡ x → y ≡ z → x ≡ z
x ≡˘〈 p 〉 q = (sym p) ∙ q

_≡〈〉_ : ∀ {ℓ} {A : Type ℓ} (x : A) {y : A} → x ≡ y → x ≡ y
x ≡〈〉 p = p

_∎ : ∀ {ℓ} {A : Type ℓ} (x : A) → x ≡ x
x ∎ = refl

infixr 30 _∙_
infixr 2 _≡〈〉_ _≡˘〈_〉_
infix  3 _∎

record Precategory (o h : Level) : Type (lsuc (o ⊔ h)) where
  no-eta-equality
  
  field
    Ob : Type o
    Hom : Ob → Ob → Type h
    id : ∀ {x} → Hom x x
    _∘_ : ∀ {x y z} → Hom y z → Hom x y → Hom x z
  
  infixr 40 _∘_
  
  field
    idr : ∀ {x y} (f : Hom x y) → f ∘ id ≡ f
    idl : ∀ {x y} (f : Hom x y) → id ∘ f ≡ f
    assoc : ∀ {w x y z} (f : Hom y z) (g : Hom x y) (h : Hom w x)
          → f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h

record InvariantFunctor
  {o₁ h₁ o₂ h₂}
  (C : Precategory o₁ h₁)
  (D : Precategory o₂ h₂)
  : Type (o₁ ⊔ h₁ ⊔ o₂ ⊔ h₂)
  where
  no-eta-equality
  
  private
    module C = Precategory C
    module D = Precategory D
  
  field
    F₀ : C.Ob → D.Ob
    F₁ : ∀ {x y} → C.Hom x y → C.Hom y x → D.Hom (F₀ x) (F₀ y)
  
  field
    F-id : ∀ {x} → F₁ (C.id {x}) (C.id {x}) ≡ D.id
    F-∘ : ∀ {x y z}
        → (f : C.Hom x y) (g : C.Hom y x)
        → (h : C.Hom y z) (j : C.Hom z y)
        → F₁ (h C.∘ f) (g C.∘ j) ≡ (F₁ h j) D.∘ (F₁ f g)

module _ {o₁ h₁ o₂ h₂} (C : Precategory o₁ h₁) (D : Precategory o₂ h₂) (F : InvariantFunctor C D) where
  private module C = Precategory C
  private module D = Precategory D
  private module F = InvariantFunctor F
  
  imap-iso-is-iso : ∀ {x y : C.Ob} (f : C.Hom x y) (g : C.Hom y x)
                  → (p : f C.∘ g ≡ C.id)
                  → (F.F₁ f g) D.∘ (F.F₁ g f) ≡ D.id
  imap-iso-is-iso f g p = 
    (F.F₁ f g) D.∘ (F.F₁ g f) ≡〈 sym (F.F-∘ g f f g) 〉
    F.F₁ (f C.∘ g) (f C.∘ g)  ≡〈 ap (λ l → F.F₁ l (f C.∘ g)) p 〉
    F.F₁ C.id (f C.∘ g)       ≡〈 ap (λ r → F.F₁ C.id r) p 〉
    F.F₁ C.id C.id            ≡〈 F.F-id 〉
    D.id                      ∎