blob: dcc72d6dbc927b4c8c96504e3da67634c489533c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level)
module SplitIdempotents.Setoids {c ℓ : Level} where
open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Category.KaroubiComplete (Setoids c ℓ) using (KaroubiComplete)
open import Function using (Func; _⟶ₛ_; _⟨$⟩_; id)
open import Function.Construct.Identity using () renaming (function to Id)
open import Function.Construct.Setoid using (_∙_)
open import Relation.Binary using (Setoid)
open Func using (cong)
module _ {S : Setoid c ℓ} (f : S ⟶ₛ S) where
private
module S = Setoid S
Q : Setoid c ℓ
Q = record
{ Carrier = S.Carrier
; _≈_ = λ a b → f ⟨$⟩ a S.≈ f ⟨$⟩ b
; isEquivalence = record
{ refl = S.refl
; sym = S.sym
; trans = S.trans
}
}
to : S ⟶ₛ Q
to = record
{ to = id
; cong = cong f
}
from : Q ⟶ₛ S
from = record
{ to = f ⟨$⟩_
; cong = id
}
Setoids-KaroubiComplete : KaroubiComplete
Setoids-KaroubiComplete = record
{ split = λ {A} {f} idem → record
{ obj = Q f
; retract = to f
; section = from f
; retracts = idem
; splits = Setoid.refl A
}
}
|
