\begin{code}
{-# OPTIONS --safe #-}

module Examples.Quotients where

open import Prelude hiding (_/_; [_]; eq/; squash/; rec/; isSet; isProp; elim/; ∥_∥)

\end{code}
\begin{code}
isProp : Type → Type
\end{code}
%<*is-prop>
\begin{code}
isProp P = (x y : P) → x ≡ y
\end{code}
%</is-prop>


\begin{code}
isSet : Type → Type
\end{code}
%<*is-set>
\begin{code}[number=eq:isSet]
isSet B = (x y : B) → (p q : x ≡ y) → p ≡ q
\end{code}
%</is-set>

%<*quot-def>
\begin{code}[number=quot-def]
data _/_ (A : Type) (_~_ : A → A → Type) : Type where
  [_] : A → A / _~_
  eq/ : (x y : A) → x ~ y → [ x ] ≡ [ y ]
  squash/ : isSet (A / _~_)
\end{code}
%</quot-def>

\begin{code}
module _ {A : Type} {_~_ : A → A → Type} {B : Type} where
\end{code}
%<*rec-head>
\begin{code}
  rec/ :  isSet B
      →   (f : A → B)
      →   (∀ x y → x ~ y → f x ≡ f y)
      →   A / _~_ → B
  rec/ set f resp = ϕ where
\end{code}
%</rec-head>
%<*rec-body>
\begin{code}[number=rec-impl]
    ϕ : A / _~_ → B
    ϕ [ x ]                  = f x
    ϕ (eq/ x y x~y i)        = resp x y x~y i
    ϕ (squash/ x y p q i j)  =
      set (ϕ x) (ϕ y) (cong ϕ p) (cong ϕ q) i j
\end{code}
%</rec-body>
%<*prop-trunc>
\begin{code}
∥_∥ : Type → Type
∥ A ∥ = A / λ _ _ → ⊤
\end{code}
%</prop-trunc>