{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Groupoid
 
module Categories.Category.Groupoid.Properties {o ℓ e} (G : Groupoid o ℓ e) where
 
import Categories.Morphism as Morphism
import Categories.Morphism.Properties as MorphismProps
import Categories.Morphism.Reasoning as MR
 
open Groupoid G
open Morphism category
open MorphismProps category
open HomReasoning
open MR category
 
private
  variable
    A B C : Obj
 
mono : {f : A ⇒ B} → Mono f
mono = Iso⇒Mono iso
 
epi : {f : A ⇒ B} → Epi f
epi = Iso⇒Epi iso
 
id-inverse : id {A = A} ⁻¹ ≈ id
id-inverse = ⟺ identityˡ ○ iso.isoʳ
 
⁻¹-involutive : {f : A ⇒ B} → f ⁻¹ ⁻¹ ≈ f
⁻¹-involutive {f = f} = begin
  f ⁻¹ ⁻¹            ≈⟨ introʳ iso.isoˡ ⟩
  f ⁻¹ ⁻¹ ∘ f ⁻¹ ∘ f ≈⟨ sym-assoc ○ elimˡ iso.isoˡ ⟩
                   f ∎
 
⁻¹-commute : {f : A ⇒ B} {g : C ⇒ A} → (f ∘ g) ⁻¹ ≈ g ⁻¹ ∘ f ⁻¹
⁻¹-commute {f = f} {g} = epi _ _ ( begin
  (f ∘ g) ⁻¹ ∘ f ∘ g    ≈⟨ iso.isoˡ ⟩
  id                    ≈˘⟨ iso.isoˡ ⟩
  g ⁻¹ ∘ g              ≈˘⟨ cancelInner iso.isoˡ ⟩
  (g ⁻¹ ∘ f ⁻¹) ∘ f ∘ g ∎ )