{-# OPTIONS --erased-cubical --safe #-}
import Equality.Path as P
module Quotient.Erased.Basics
{e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where
open P.Derived-definitions-and-properties eq hiding (elim)
open import Prelude
open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
import H-level P.equality-with-J as PH
open import H-level.Closure equality-with-J
private
variable
a b p r : Level
A B : Type a
R : A → A → Type r
x y : A
infix 5 _/ᴱ_
data _/ᴱ_ (A : Type a) (@0 R : A → A → Type r) : Type (a ⊔ r) where
[_] : A → A /ᴱ R
@0 []-respects-relationᴾ : {x y : A} → R x y → [ x ] P.≡ [ y ]
@0 /ᴱ-is-setᴾ : P.Is-set (A /ᴱ R)
@0 []-respects-relation : R x y → _≡_ {A = A /ᴱ R} [ x ] [ y ]
[]-respects-relation = _↔_.from ≡↔≡ ∘ []-respects-relationᴾ
@0 /ᴱ-is-set : Is-set (A /ᴱ R)
/ᴱ-is-set = _↔_.from (H-level↔H-level 2) /ᴱ-is-setᴾ
record Elimᴾ′ {A : Type a} {@0 R : A → A → Type r}
(P : A /ᴱ R → Type p) :
Type (a ⊔ r ⊔ p) where
no-eta-equality
field
[]ʳ : ∀ x → P [ x ]
@0 []-respects-relationʳ :
(r : R x y) →
P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y
@0 is-setʳ :
{eq₁ eq₂ : x P.≡ y} {p : P x} {q : P y}
(eq₃ : P.[ (λ i → P (eq₁ i)) ] p ≡ q)
(eq₄ : P.[ (λ i → P (eq₂ i)) ] p ≡ q) →
P.[ (λ i → P.[ (λ j → P (/ᴱ-is-setᴾ eq₁ eq₂ i j)) ] p ≡ q) ]
eq₃ ≡ eq₄
open Elimᴾ′ public
elimᴾ′ :
{@0 R : A → A → Type r}
{P : A /ᴱ R → Type p} →
Elimᴾ′ P → (x : A /ᴱ R) → P x
elimᴾ′ {A} {R} {P} e = helper
where
module E = Elimᴾ′ e
helper : (x : A /ᴱ R) → P x
helper [ x ] = E.[]ʳ x
helper ([]-respects-relationᴾ r i) = E.[]-respects-relationʳ r i
helper (/ᴱ-is-setᴾ p q i j) =
E.is-setʳ (λ i → helper (p i)) (λ i → helper (q i)) i j
record Elimᴾ {A : Type a} {@0 R : A → A → Type r}
(P : A /ᴱ R → Type p) :
Type (a ⊔ r ⊔ p) where
no-eta-equality
field
[]ʳ : ∀ x → P [ x ]
@0 []-respects-relationʳ :
(r : R x y) →
P.[ (λ i → P ([]-respects-relationᴾ r i)) ] []ʳ x ≡ []ʳ y
@0 is-setʳ : ∀ x → P.Is-set (P x)
open Elimᴾ public
elimᴾ :
{@0 R : A → A → Type r}
{P : A /ᴱ R → Type p} →
Elimᴾ P → (x : A /ᴱ R) → P x
elimᴾ e = elimᴾ′ λ where
.[]ʳ → E.[]ʳ
.[]-respects-relationʳ → E.[]-respects-relationʳ
.is-setʳ → P.heterogeneous-UIP E.is-setʳ _
where
module E = Elimᴾ e
private
elimᴾ′₂ :
{@0 R : A → A → Type r}
{P : A /ᴱ R → Type p} →
Elimᴾ′ P → (x : A /ᴱ R) → P x
elimᴾ′₂ {P} e = elimᴾ λ where
.[]ʳ → E.[]ʳ
.[]-respects-relationʳ → E.[]-respects-relationʳ
.is-setʳ x {x = y} {y = z} p q → $⟨ E.is-setʳ p q ⟩
P.[ (λ i →
P.[ (λ j → P (/ᴱ-is-setᴾ P.refl P.refl i j)) ] y ≡ z) ]
p ≡ q ↝⟨ P.subst (λ eq → P.[ (λ i → P.[ (λ j → P (eq i j)) ] y ≡ z) ] p ≡ q)
(PH.mono₁ 2 /ᴱ-is-setᴾ _ _) ⟩
P.[ (λ _ → P.[ (λ _ → P x) ] y ≡ z) ] p ≡ q ↔⟨⟩
p P.≡ q □
where
module E = Elimᴾ′ e
record Recᴾ {A : Type a} (@0 R : A → A → Type r) (B : Type b) :
Type (a ⊔ r ⊔ b) where
no-eta-equality
field
[]ʳ : A → B
@0 []-respects-relationʳ : (r : R x y) → []ʳ x P.≡ []ʳ y
@0 is-setʳ : P.Is-set B
open Recᴾ public
recᴾ :
{@0 R : A → A → Type r} →
Recᴾ R B → A /ᴱ R → B
recᴾ r = elimᴾ λ where
.[]ʳ → R.[]ʳ
.[]-respects-relationʳ → R.[]-respects-relationʳ
.is-setʳ _ → R.is-setʳ
where
module R = Recᴾ r
record Elim {A : Type a} {@0 R : A → A → Type r}
(P : A /ᴱ R → Type p) :
Type (a ⊔ r ⊔ p) where
no-eta-equality
field
[]ʳ : ∀ x → P [ x ]
@0 []-respects-relationʳ :
(r : R x y) →
subst P ([]-respects-relation r) ([]ʳ x) ≡ []ʳ y
@0 is-setʳ : ∀ x → Is-set (P x)
open Elim public
elim :
{@0 R : A → A → Type r}
{P : A /ᴱ R → Type p} →
Elim P → (x : A /ᴱ R) → P x
elim e = elimᴾ λ where
.[]ʳ → E.[]ʳ
.[]-respects-relationʳ → subst≡→[]≡ ∘ E.[]-respects-relationʳ
.is-setʳ → _↔_.to (H-level↔H-level 2) ∘ E.is-setʳ
where
module E = Elim e
record Rec {A : Type a} (@0 R : A → A → Type r) (B : Type b) :
Type (a ⊔ r ⊔ b) where
no-eta-equality
field
[]ʳ : A → B
@0 []-respects-relationʳ : (r : R x y) → []ʳ x ≡ []ʳ y
@0 is-setʳ : Is-set B
open Rec public
rec :
{@0 R : A → A → Type r} →
Rec R B → A /ᴱ R → B
rec r = recᴾ λ where
.[]ʳ → R.[]ʳ
.[]-respects-relationʳ → _↔_.to ≡↔≡ ∘ R.[]-respects-relationʳ
.is-setʳ → _↔_.to (H-level↔H-level 2) R.is-setʳ
where
module R = Rec r
record Elim-prop
{A : Type a} {@0 R : A → A → Type r}
(P : A /ᴱ R → Type p) :
Type (a ⊔ r ⊔ p) where
no-eta-equality
field
[]ʳ : ∀ x → P [ x ]
@0 is-propositionʳ : ∀ x → Is-proposition (P [ x ])
open Elim-prop public
elim-prop :
{@0 R : A → A → Type r}
{P : A /ᴱ R → Type p} →
Elim-prop P → (x : A /ᴱ R) → P x
elim-prop e = elim λ where
.[]ʳ → E.[]ʳ
.[]-respects-relationʳ _ → E.is-propositionʳ _ _ _
.is-setʳ → elim λ @0 where
.[]ʳ → mono₁ 1 ∘ E.is-propositionʳ
.[]-respects-relationʳ _ → H-level-propositional ext 2 _ _
.is-setʳ _ → mono₁ 1 (H-level-propositional ext 2)
where
module E = Elim-prop e
record Rec-prop (A : Type a) (B : Type b) : Type (a ⊔ b) where
no-eta-equality
field
[]ʳ : A → B
@0 is-propositionʳ : Is-proposition B
open Rec-prop public
rec-prop :
{@0 R : A → A → Type r} →
Rec-prop A B → A /ᴱ R → B
rec-prop r = elim-prop λ where
.[]ʳ → R.[]ʳ
.is-propositionʳ _ → R.is-propositionʳ
where
module R = Rec-prop r