{-# OPTIONS --without-K #-}
module segal.equivalences where

open import function.isomorphism
open import level
open import sum

open import segal.composition
open import segal.identities

SegalDeg₁ : (i : Level) → Set (lsuc i)
SegalDeg₁ i = Σ (Segal₁ i) HasDeg₁

WildId₁ : (i : Level) → Set (lsuc i)
WildId₁ i = Σ (Wild₁ i) HasId₁

segal-deg-wild-id₁ : ∀ {i} → SegalDeg₁ i ≅ WildId₁ i
segal-deg-wild-id₁ = Σ-ap-iso' segal-wild₁ λ _ → deg-id₁

SegalDeg₂ : (i : Level) → Set (lsuc i)
SegalDeg₂ i = Σ (Segal₂ i) HasDeg₂

WildId₂ : (i : Level) → Set (lsuc i)
WildId₂ i = Σ (Wild₂ i) HasId₂

segal-deg-wild-id₂ : ∀ {i} → SegalDeg₂ i ≅ WildId₂ i
segal-deg-wild-id₂ = Σ-ap-iso' segal-wild₂ λ _ → deg-id₂

SegalDeg₃ : (i : Level) → Set (lsuc i)
SegalDeg₃ i = Σ (Segal₃ i) HasDeg₃

WildId₃ : (i : Level) → Set (lsuc i)
WildId₃ i = Σ (Wild₃ i) HasId₃

segal-deg-wild-id₃ : ∀ {i} → SegalDeg₃ i ≅ WildId₃ i
segal-deg-wild-id₃ = Σ-ap-iso' segal-wild₃ λ _ → deg-id₃