{-# OPTIONS --without-K #-}
open import Agda.Primitive
open import 1-equality
open import 2-composition
open import 3-ap
open import 4-homotopy
open import 5-qip
open import 6-equivalence
data Bool : Set where
true : Bool
false : Bool
isContr :
{ℓ : Level} →
(X : Set ℓ) →
Set ℓ
isContr X = Σ X λ x → Π X λ y → x ≡ y
isProp :
{ℓ : Level} →
(X : Set ℓ) →
Set ℓ
isProp X = (x y : X) → isContr (x ≡ y)
isSet :
{ℓ : Level} →
(X : Set ℓ) →
Set ℓ
isSet X = (x y : X) → isProp (x ≡ y)
is·monic :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
Set (ℓ₁ ⊔ ℓ₂)
is·monic {A = A} {B = B} f =
(g h : B → A) →
(f ∘ g ∼ f ∘ h) →
g ∼ h
monic·theorem :
{ℓ₁ ℓ₂ ℓ₃ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
{C : Set ℓ₃} →
(f : A → B) →
(is·monic f) →
(g h : C → A) →
((f ∘ g) ∼ (f ∘ h)) →
g ∼ h
monic·theorem f imf g h fg∼fh =
λ c → imf (λ _ → g c)
(λ _ → h c)
(λ _ → fg∼fh c)
((f ∘ h) c)
is·injective :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
Set (ℓ₁ ⊔ ℓ₂)
is·injective {A = A} {B = B} f =
(x y : A) →
f x ≡ f y →
(x ≡ y)
is·injective·to·is·monic :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
is·injective f → is·monic f
is·injective·to·is·monic f iif =
λ g h f∘g∼f∘h z → iif (g z) (h z) (f∘g∼f∘h z)
is·monic·to·is·injective :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
is·monic f → is·injective f
is·monic·to·is·injective f imf =
λ x y fx≡fy →
imf (λ _ → x) (λ _ → y) (λ _ → fx≡fy) (f x)
monic·injective·homotopy·1 :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
is·monic·to·is·injective f ∘ is·injective·to·is·monic f ∼ id
monic·injective·homotopy·1 f = λ _ → refl
is·epic :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
Set (ℓ₁ ⊔ ℓ₂)
is·epic {A = A} {B = B} f =
(g h : B → A) →
(g ∘ f ∼ h ∘ f) →
g ∼ h
is·surjective :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
Set (ℓ₁ ⊔ ℓ₂)
is·surjective {A = A} {B = B} f =
(b : B) → Σ A λ a → f a ≡ b
surjective·theorem :
{ℓ₁ ℓ₂ ℓ₃ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
{C : Set ℓ₃} →
(f : A → B) →
(is·surjective f) →
(g h : B → C) →
(g ∘ f ∼ h ∘ f) →
g ∼ h
surjective·theorem f isf g h gf∼hf b =
gb≡gfa • gfa≡hfa • hfa≡hb
where
a = Σ.fst (isf b)
fa≡b = Σ.snd (isf b)
gb≡gfa = sym (ap g fa≡b)
gfa≡hfa = gf∼hf a
hfa≡hb = ap h fa≡b
is·surjective·to·is·epic :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
is·surjective f → is·epic f
is·surjective·to·is·epic = surjective·theorem
is·epic+ :
{ℓ₁ ℓ₂ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
(f : A → B) →
Set (lsuc (ℓ₁ ⊔ ℓ₂))
is·epic+ {ℓ₁ = ℓ₁} {ℓ₂ = ℓ₂} {A = A} {B = B} f =
(C : Set (ℓ₁ ⊔ ℓ₂)) →
(g h : B → C) →
(g ∘ f ∼ h ∘ f) →
g ∼ h
epi·monic·1 :
{ℓ₁ ℓ₂ ℓ₃ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
{C : Set ℓ₃} →
(f : B → A) →
(g : A → B) →
(u v : C → A) →
(f ∘ g ∼ id) →
(g ∘ u ∼ g ∘ v) →
u ∼ v
epi·monic·1 {A = A} {B = B} {C = C} f g u v fg∼id gu∼gv =
λ x → g·monic (u x) (v x) (gu∼gv x)
where
g·monic : (a₁ a₂ : A) → g a₁ ≡ g a₂ → a₁ ≡ a₂
g·monic a₁ a₂ ga₁≡ga₂ =
(sym (fg∼id a₁)) • (ap f ga₁≡ga₂) • (fg∼id a₂)
epi·monic·2 :
{ℓ₁ ℓ₂ ℓ₃ : Level} →
{A : Set ℓ₁} →
{B : Set ℓ₂} →
{C : Set ℓ₃} →
(f : B → A) →
(g : A → B) →
(u v : A → C) →
(f ∘ g ∼ id) →
(u ∘ f ∼ v ∘ f) →
u ∼ v
epi·monic·2 {A = A} {B = B} {C = C} f g u v fg∼id uf∼vf a =
(ap u (sym fb≡a)) • (uf∼vf b) • (ap v fb≡a)
where
f·epi : (a : A) → Σ B (λ b → f b ≡ a)
f·epi a = [ g a , fg∼id a ]
b = Σ.fst (f·epi a)
fb≡a = Σ.snd (f·epi a)