{-# OPTIONS --without-K #-}
module segal.identities.l1 where

open import equality
open import function.isomorphism

open import segal.composition.l1

record HasId₁ {i} (W : Wild₁ i) : Set i where
  constructor mk-id₁
  field
    id : (x : obj W) → hom W x x

record HasDeg₁ {i} (X : Segal₁ i) : Set i where
  constructor mk-deg₁
  open Segal₁ X
  field
    s00 : (x : X₀) → X₁ x x

module _ {i} {W : Wild₁ i} where
  private X = invert≅ segal-wild₁ W

  deg-id₁ : HasDeg₁ X ≅ HasId₁ W
  deg-id₁ = record
    { to = λ { (mk-deg₁ s00) → mk-id₁ s00 }
    ; from = λ { (mk-id₁ id) → mk-deg₁ id }
    ; iso₁ = λ _ → refl
    ; iso₂ = λ _ → refl }