module Axioms where
open import Prelude public
postulate
propext :
{l : Level}
{P Q : Prop l}
→
(P ↔ Q) → P ≡ Q
module quot where
postulate
ty :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
→
Set l
mk :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
→
A → ty R
eq :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
{x y : A}
→
R x y → mk R x ≡ mk R y
elim :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
{n : Level}
(B : ty R → Set n)
(f : ∀ x → B (mk R x))
(_ : ∀ {x y} → R x y → f x ≣ f y)
→
∀ t → B t
comp :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
{n : Level}
(B : ty R → Set n)
(f : ∀ x → B (mk R x))
(e : ∀ {x y} → R x y → f x ≣ f y)
→
∀ x → elim R B f e (mk R x) ≡ f x
{-# REWRITE comp #-}
lift :
{l m : Level}
{A : Set l}
{R : A → A → Prop m}
{n : Level}
{B : Set n}
(f : A → B)
(_ : ∀ {x y} → R x y → f x ≡ f y)
→
ty R → B
lift = elim _ (λ _ → _)
liftcomp :
{l m : Level}
{A : Set l}
{R : A → A → Prop m}
{n : Level}
{B : Set n}
(f : A → B)
(e : ∀ {x y} → R x y → f x ≡ f y)
→
∀ x → lift f e (mk R x) ≡ f x
liftcomp = λ _ _ _ → refl
ind :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
{n : Level}
(P : ty R → Prop n)
(f : ∀ x → P (mk R x))
→
∀ t → P t
ind R P f t =
↓prop (elim R
(LiftProp ∘ P)
(λ x → ↑prop (f x))
(λ r → ≣irrel (ap P (eq R r)))
t)
surjectionmk :
{l m : Level}
{A : Set l}
(R : A → A → Prop m)
→
surjection (mk R)
surjectionmk {A = A} R =
ind R (λ z → ∃ x ∶ A , mk R x ≡ z) λ x → (∃i x refl)
funext :
{l m : Level}
{A : Set l}
{B : A → Set m}
{f g : (x : A) → B x}
(_ : ∀ x → f x ≡ g x)
→
f ≡ g
funext {A = A} {B} {f} {g} e = ap m (eq 𝕀₂ {x = O} {I} ⊤i)
where
data 𝕀 : Set where
O : 𝕀
I : 𝕀
𝕀₂ : 𝕀 → 𝕀 → Prop
𝕀₂ _ _ = ⊤
k : (x : A) → 𝕀 → B x
k x O = f x
k x I = g x
l : (x : A)(i j : 𝕀) → 𝕀₂ i j → k x i ≡ k x j
l x O O _ = refl
l x O I _ = e x
l x I O _ = symm (e x)
l x I I _ = refl
m : ty 𝕀₂ → (x : A) → B x
m z x = elim 𝕀₂ (λ _ → B x) (k x) (λ {i} {j} _ → l x i j ⊤i) z
lift₂ :
{l l' m m' : Level}
{A : Set l}
{R : A → A → Prop m}
{B : Set l'}
{S : B → B → Prop m'}
{n : Level}
{C : Set n}
(f : A → B → C)
(_ : ∀ {x x' y } → R x x' → f x y ≡ f x' y )
(_ : ∀ {x y y'} → S y y' → f x y ≡ f x y')
→
ty R → ty S → C
lift₂ {S = S} f e₁ e₂ =
lift
(λ x → lift (λ y → f x y) e₂)
(λ {x} {x'} r →
funext (ind S
(λ z → lift (λ y → f x y) e₂ z ≡ lift (λ y → f x' y) e₂ z)
(λ _ → e₁ r)))
ind₂ :
{l l' m m' : Level}
{A : Set l}
(R : A → A → Prop m)
{B : Set l'}
(S : B → B → Prop m')
{n : Level}
(P : ty R → ty S → Prop n)
(f : ∀ x y → P (mk R x) (mk S y))
→
∀ r s → P r s
ind₂ R S P f =
ind R (λ r → ∀ s → P r s) (λ x →
ind S (P (mk R x)) (f x))
infix 6 _/_ [_]/_
_/_ : {l m : Level}(A : Set l)(R : A → A → Prop m) → Set l
A / R = quot.ty R
[_]/_ : {l m : Level}{A : Set l} → A → (R : A → A → Prop m) → A / R
[ x ]/ R = quot.mk R x
quot-eff :
{l : Level}
{A : Set l}
(R S : A → A → Prop l)
(R⊆S : ∀{x y} → R x y → S x y)
(Srefl : ∀{x y} → x ≡ y → S x y)
(Ssymm : ∀{x y} → S x y → S y x)
(Strans : ∀{x y z} → S y z → S x y → S x z)
→
∀{x y} → [ x ]/ R ≡ [ y ]/ R → S x y
quot-eff {l} {A} R S R⊆S Srefl Ssymm Strans p = r p
where
f : ∀{x x' y} → R x x' → S x y ≡ S x' y
f p = propext
(∧i (λ q → Strans q (Ssymm (R⊆S p))) (λ q → Strans q (R⊆S p)))
g : ∀{x y y'} → R y y' → S x y ≡ S x y'
g p = propext
(∧i (λ q → Strans (R⊆S p) q) (λ q → Strans (Ssymm (R⊆S p)) q))
S' : A / R → A / R → Prop l
S' = quot.lift₂ S f g
r : {z z' : A / R} → z ≡ z' → S' z z'
r {z} refl =
quot.ind R (λ z → S' z z) (λ _ → Srefl refl) z
funext :
{l m : Level}
{A : Set l}
{B : A → Set m}
{f g : (x : A) → B x}
(_ : ∀ x → f x ≡ g x)
→
f ≡ g
funext = quot.funext
funexp :
{l m : Level}
{A : Prop l}
{B : A → Set m}
{f g : (x : A) → B x}
(_ : ∀ x → f x ≡ g x)
→
f ≡ g
funexp {A = A} {B} {f} {g} e = ap f=g (eq O=I {x = O} {I} ⊤i)
where
open quot
data 𝕀 : Set where
O : 𝕀
I : 𝕀
O=I : 𝕀 → 𝕀 → Prop
O=I _ _ = ⊤
fg : (x : A) → 𝕀 → B x
fg x O = f x
fg x I = g x
h : (x : A)(i j : 𝕀) → O=I i j → fg x i ≡ fg x j
h x O O _ = refl
h x O I _ = e x
h x I O _ = symm (e x)
h x I I _ = refl
f=g : ty O=I → (x : A) → B x
f=g z x =
elim O=I (λ _ → B x) (fg x) (λ {i} {j} _ → h x i j ⊤i) z
heq-funext :
{l m : Level}
{A A' : Set l}
{B : A → Set m}
{B' : A' → Set m}
{f : (x : A) → B x}
{f' : (x : A') → B' x}
(_ : A ≡ A')
(_ : ∀{x x'} → x ≣ x' → f x ≣ f' x')
→
f ≣ f'
heq-funext refl e with funext (λ x → (≣typ (e{x}{x} refl)))
... | refl = funext λ x → e{x}{x} refl
heq-funexp :
{l m : Level}
{A : Prop l}
{B C : Set m}
{f : A → B}
{g : A → C}
(_ : B ≡ C)
(_ : ∀ x → f x ≣ g x)
→
f ≣ g
heq-funexp refl e' = funexp e'
heq-funexp' :
{l m : Level}
{A B : Prop l}
{C : Set m}
{f : A → C}
{g : B → C}
(_ : A ≡ B)
(_ : ∀ x y → f x ≣ g y)
→
f ≣ g
heq-funexp' refl e = funexp λ x → e x x
implicit-funext :
{l m : Level}
{A : Set l}
{B : A → Set m}
{f g : {x : A} → B x}
(_ : ∀ x → f {x} ≡ g {x})
→
(λ{x} → f {x}) ≡ (λ{x} → g {x})
implicit-funext {A = A} {B} {f} {g} e =
ap impl (funext {f = λ x → f{x}} {g = λ x → g{x}} e)
where
impl : ((x : A) → B x) → {x : A} → B x
impl f {x} = f x
instance-funext :
{l m : Level}
{A : Set l}
{B : A → Set m}
{f g : {{x : A}} → B x}
(_ : ∀ x → f {{x}} ≡ g {{x}})
→
(λ{{x}} → f {{x}}) ≡ (λ{{x}} → g {{x}})
instance-funext {A = A} {B} {f} {g} e =
ap sett (funext {f = λ x → f{{x}}} {g = λ x → g{{x}}} e)
where
sett : ((x : A) → B x) → {{x : A}} → B x
sett f {{x}} = f x
instance-funexp :
{l m : Level}
{A : Prop l}
{B : A → Set m}
{f g : {{x : A}} → B x}
(_ : ∀ x → f {{x}} ≡ g {{x}})
→
(λ{{x}} → f {{x}}) ≡ (λ{{x}} → g {{x}})
instance-funexp {A = A} {B} {f} {g} e =
ap sett (funexp {f = λ x → f{{x}}} {g = λ x → g{{x}}} e)
where
sett : ((x : A) → B x) → {{x : A}} → B x
sett f {{x}} = f x
postulate
A!C : {l : Level}{A : Set l} → (∃ x ∶ A , ∀(x' : A) → x ≡ x') → A
module _
{l m : Level}
(A : Set l)
(P : A → Prop m)
where
private
AP : Set (l ⊔ m)
AP = set A P
∃!AP : ∃! A P → ∃ z ∶ AP , ∀(z' : AP) → z ≡ z'
∃!AP (∃i x (∧i p q)) =
∃i (x ∣ p) λ{(x' ∣ p') → setext (q x' p')}
the : {{∃! A P}} → A
the {{u}} = el (A!C (∃!AP u))
the-pf : {{_ : ∃! A P}} → P the
the-pf {{u}} = pf (A!C (∃!AP u))
the-uniq : {{_ : ∃! A P}}(x : A) → P x → the ≡ x
the-uniq {{∃i x' (∧i p' q)}} x p =
let
instance
_ : ∃! A P
_ = ∃i x' (∧i p' q)
in
symm (q the the-pf) ; q x p
syntax the A (λ x → P) = the x ∶ A , P
coe :
{l : Level}
{A B : Set l}
→
A ≡ B → A → B
coe {A = A} {B} e x = the B (_≣ x) {{coe! e}}
module _ where
coe! : A ≡ B → ∃! y ∶ B , y ≣ x
coe! refl = ∃i x (∧i refl λ _ p → symm p)
coerefl :
{l : Level}
{A : Set l}
(x : A)
→
coe refl x ≡ x
coerefl x = the-pf _ (_≣ x) {{coe! refl x refl}}
coe≣ :
{l : Level}
{A A' : Set l}
(e : A ≡ A')
(x : A)
→
coe e x ≣ x
coe≣ refl x = coerefl x
coe⁻¹ :
{l : Level}
{A B : Set l}
→
A ≡ B → B → A
coe⁻¹ e = coe (symm e)
coe⁻¹coe :
{l : Level}
{A B : Set l}
(e : A ≡ B)
{x : A}
→
coe⁻¹ e (coe e x) ≡ x
coe⁻¹coe refl {x} =
proof
coe refl (coe refl x)
=[ coerefl _ ]
coe refl x
=[ coerefl _ ]
x
qed
coecoe⁻¹ :
{l : Level}
{A B : Set l}
(e : A ≡ B)
{y : B}
→
coe e (coe⁻¹ e y) ≡ y
coecoe⁻¹ refl {y} =
proof
coe refl (coe refl y)
=[ coerefl _ ]
coe refl y
=[ coerefl _ ]
y
qed
coe=id :
{l : Level}
{A A' : Set l}
(e : A ≡ A')
→
coe e ≣ λ (x : A) → x
coe=id refl = funext coerefl
∘coe :
{l m : Level}
{A A' : Set l}
{B : Set m}
(e : A ≡ A')
(f : A' → B)
→
f ∘ coe e ≣ f
∘coe refl f = ap (f ∘_) (coe=id refl)
coe∘ :
{l m : Level}
{A : Set l}
{B B' : Set m}
(e : B ≡ B')
(f : A → B)
→
coe e ∘ f ≣ f
coe∘ refl f = ap (_∘ f) (coe=id refl)
subst :
{l m : Level}
{A : Set l}
(B : A → Set m)
{x x' : A}
(e : x ≡ x')
→
B x → B x'
subst B e = coe (ap B e)
subst≣ :
{l m : Level}
{A : Set l}
(B : A → Set m)
{x x' : A}
(e : x ≡ x')
(y : B x)
→
subst B e y ≣ y
subst≣ _ refl = coerefl
substrefl :
{l m : Level}
{A : Set l}
(B : A → Set m)
{x : A}
(y : B x)
→
subst B refl y ≡ y
substrefl _ = coerefl