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

open import equality
open import level
open import function.isomorphism
open import sum

record Wild₁ (i : Level) : Set (lsuc i) where
  constructor mk-wild
  field obj : Set i
  field hom : obj → obj → Set i
open Wild₁ public

record Segal₁ (i : Level) : Set (lsuc i) where
  constructor mk-segal
  field X₀ : Set i
  field X₁ : X₀ → X₀ → Set i

Δ¹ : ∀ {i} → Segal₁ i → Set i
Δ¹ X = Σ X₀ λ x0 → Σ X₀ λ x1 → X₁ x0 x1
  where open Segal₁ X

segal-wild₁ : ∀ {i} → Segal₁ i ≅ Wild₁ i
segal-wild₁ = record
  { to = λ {(mk-segal o h) → mk-wild o h}
  ; from = λ {(mk-wild o h) → mk-segal o h}
  ; iso₁ = λ {(mk-segal o h) → refl}
  ; iso₂ = λ {(mk-wild o h) → refl} }