https://gist.github.com/andrejbauer/65ee1ae98167e6411e512d3e5a36c086#file-setoidchoice-agda

SetoidChoice_.agda

    canonical-elements⇒type-like : is-set Carrier → canonical-elements → type-like c
    canonical-elements⇒type-like set
      record { canon = canon
             ; canon-≈ = canon-≈
             ; canon-≡ = canon-≡ }
      =
      record { type-like-to = Σ _ λ a → canon a ≡ a
             ; type-like-≅ = record { iso = record { _⟨$⟩_ = λ a → canon a , canon-≡ _ _ (canon-≈ a)
                                                   ; cong = λ s → Σ-≡ (canon-≡ _ _ s) set }
                                    ; inv = record { _⟨$⟩_ = fst
                                                   ; cong = λ s → Setoid.reflexive A (≡-cong fst s) }
                                    ; iso-inv = λ y → Σ-≡ (snd y) set
                                    ; inv-iso = canon-≈ } }