Skip to content

Commit 34711fc

Browse files
JacquesCaretteJacquesCarette
committed
final pass of cleaning up
1 parent 9b206d7 commit 34711fc

File tree

12 files changed

+99
-96
lines changed

12 files changed

+99
-96
lines changed

‎src/Categories/Category/Instance/Setoids.agda‎

Lines changed: 15 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -4,30 +4,31 @@ module Categories.Category.Instance.Setoids where
44
-- Category of Setoids, aka (Setoid, _⟶_, Setoid ≈)
55
-- Note the (explicit) levels in each
66

7-
open import Level
8-
open import Relation.Binary
9-
open import Function.Bundles
7+
open import Level using (suc; _⊔_)
8+
open import Relation.Binary.Bundles using (Setoid)
9+
open import Function.Bundles using (Func; _⟨$⟩_)
10+
open import Function.Base using (_$_)
1011
import Function.Construct.Composition as Comp
1112
import Function.Construct.Identity as Id
13+
import Function.Construct.Setoid as S
1214

13-
open import Categories.Category
15+
open import Categories.Category.Core using (Category)
16+
17+
open Func
18+
open Setoid
1419

1520
Setoids : ∀ c ℓ → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
1621
Setoids c ℓ = record
1722
{ Obj = Setoid c ℓ
1823
; _⇒_ = Func
19-
; _≈_ = λ {A B} → λ f g → ∀ {x y} → Setoid._≈_ A x y → Setoid._≈_ B (f ⟨$⟩ x) (g ⟨$⟩ y)
24+
; _≈_ = λ {A} {B} f g → _≈_ (S.function A B) f g
2025
; id = Id.function _
2126
; _∘_ = λ f g → Comp.function g f
22-
; assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → Func.cong h (Func.cong g (Func.cong f x≈y))
23-
; sym-assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → Func.cong h (Func.cong g (Func.cong f x≈y))
24-
; identityˡ = λ {A} {B} {f} x≈y → Func.cong f x≈y
25-
; identityʳ = λ {A} {B} {f} x≈y → Func.cong f x≈y
27+
; assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y
28+
; sym-assoc = λ {A} {B} {C} {D} {f} {g} {h} x≈y → cong h $ cong g $ cong f x≈y
29+
; identityˡ = λ {A} {B} {f} x≈y → cong f x≈y
30+
; identityʳ = λ {A} {B} {f} x≈y → cong f x≈y
2631
; identity² = λ x≈y → x≈y
27-
; equiv = λ {A} {B} → record
28-
{ refl = λ {f} x≈y → Func.cong f x≈y
29-
; sym = λ f≈g x≈y → Setoid.sym B (f≈g (Setoid.sym A x≈y))
30-
; trans = λ f≈g g≈h x≈y → Setoid.trans B (f≈g x≈y) (g≈h (Setoid.refl A))
31-
}
32+
; equiv = λ {A} {B} → isEquivalence (S.function A B)
3233
; ∘-resp-≈ = λ f≈f′ g≈g′ x≈y → f≈f′ (g≈g′ x≈y)
3334
}

‎src/Categories/Category/Monoidal/Closed/IsClosed.agda‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ private
2424
module ℱ = Functor
2525

2626
open HomReasoning
27-
open adjoint using (Radjunct; Ladjunct; LRadjunct≈id; RLadjunct≈id) renaming (unit to η; counit to ε)
27+
open adjoint using (Radjunct; Ladjunct; LRadjunct≈id; RLadjunct≈id; Radjunct-resp-≈) renaming (unit to η; counit to ε)
2828

2929
-- and here we use sub-modules in the hopes of making things go faster
3030
open import Categories.Category.Monoidal.Closed.IsClosed.Identity Cl using (identity; diagonal)
@@ -67,10 +67,10 @@ closed = record
6767
}
6868
; γ-γ⁻¹-inverseᵇ = λ {X Y} →
6969
(λ {f} {y} eq → begin
70-
Radjunct y ∘ unitorˡ.to ≈⟨ (refl⟩∘⟨ ℱ.F-resp-≈ (-⊗ X) eq) ⟩∘⟨refl ⟩
71-
Radjunct ( [ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit) ∘ unitorˡ.to ≈˘⟨ (refl⟩∘⟨ ℱ.F-resp-≈ (-⊗ X) (pushˡ (ℱ.homomorphism [ X ,-]))) ⟩∘⟨refl ⟩
72-
Radjunct (Ladjunct (f ∘ unitorˡ.from)) ∘ unitorˡ.to ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
73-
(f ∘ unitorˡ.from) ∘ unitorˡ.to ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
70+
Radjunct y ∘ unitorˡ.to ≈⟨ Radjunct-resp-≈ eq ⟩∘⟨refl ⟩
71+
Radjunct ( [ id , f ]₁ ∘ [ id , unitorˡ.from ]₁ ∘ η.η unit) ∘ unitorˡ.to ≈˘⟨ Radjunct-resp-≈ (pushˡ (ℱ.homomorphism [ X ,-])) ⟩∘⟨refl ⟩
72+
Radjunct (Ladjunct (f ∘ unitorˡ.from)) ∘ unitorˡ.to ≈⟨ RLadjunct≈id ⟩∘⟨refl ⟩
73+
(f ∘ unitorˡ.from) ∘ unitorˡ.to ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
7474
f ∎
7575
) ,
7676
λ {y} {f} eq → begin

‎src/Categories/Category/Monoidal/Instance/Setoids.agda‎

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2,22 +2,24 @@
22

33
module Categories.Category.Monoidal.Instance.Setoids where
44

5-
open import Level
6-
open import Data.Product
7-
open import Data.Product.Relation.Binary.Pointwise.NonDependent
8-
open import Data.Sum
9-
open import Data.Sum.Relation.Binary.Pointwise
5+
open import Level using (_⊔_; suc)
6+
open import Data.Product.Base using (proj₁; proj₂; _,_)
7+
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (×-setoid)
8+
open import Data.Sum.Base using ([_,_]; inj₁; inj₂)
9+
open import Data.Sum.Relation.Binary.Pointwise using (⊎-setoid; inj₁; inj₂)
1010
open import Function.Bundles using (_⟨$⟩_; Func)
1111
open import Relation.Binary using (Setoid)
1212

13-
open import Categories.Category
14-
open import Categories.Category.Instance.Setoids
13+
open import Categories.Category.Core using (Category)
14+
open import Categories.Category.Instance.Setoids using (Setoids)
1515
open import Categories.Category.Cartesian using (Cartesian)
1616
open import Categories.Category.Cartesian.Monoidal using (module CartesianMonoidal)
1717
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
18-
open import Categories.Category.Cocartesian
19-
open import Categories.Category.Instance.SingletonSet
20-
open import Categories.Category.Instance.EmptySet
18+
open import Categories.Category.Cocartesian using (Cocartesian)
19+
open import Categories.Category.Instance.SingletonSet using (SingletonSetoid-⊤)
20+
open import Categories.Category.Instance.EmptySet using (EmptySetoid-⊥)
21+
22+
open Func
2123

2224
module _ {o ℓ} where
2325

@@ -40,10 +42,10 @@ module _ {o ℓ} where
4042
}
4143
; ⟨_,_⟩ = λ f g → record
4244
{ to = λ x → f ⟨$⟩ x , g ⟨$⟩ x
43-
; cong = λ eq → Func.cong f eq , Func.cong g eq
45+
; cong = λ eq → cong f eq , cong g eq
4446
}
45-
; project₁ = λ {_ h i} eq → Func.cong h eq
46-
; project₂ = λ {_ h i} eq → Func.cong i eq
47+
; project₁ = λ {_ h i} eq → cong h eq
48+
; project₂ = λ {_ h i} eq → cong i eq
4749
; unique = λ {W h i j} eq₁ eq₂ eq → A.sym (eq₁ (Setoid.sym W eq)) , B.sym (eq₂ (Setoid.sym W eq))
4850
}
4951
}
@@ -64,10 +66,10 @@ module _ {o ℓ} where
6466
; i₂ = record { to = inj₂ ; cong = inj₂ }
6567
; [_,_] = λ f g → record
6668
{ to = [ f ⟨$⟩_ , g ⟨$⟩_ ]
67-
; cong = λ { (inj₁ x) → Func.cong f x ; (inj₂ x) → Func.cong g x }
69+
; cong = λ { (inj₁ x) → cong f x ; (inj₂ x) → cong g x }
6870
}
69-
; inject₁ = λ {_} {f} → Func.cong f
70-
; inject₂ = λ {_} {_} {g} → Func.cong g
71+
; inject₁ = λ {_} {f} → cong f
72+
; inject₂ = λ {_} {_} {g} → cong g
7173
; unique = λ { {C} h≈f h≈g (inj₁ x) → Setoid.sym C (h≈f (Setoid.sym A x))
7274
; {C} h≈f h≈g (inj₂ x) → Setoid.sym C (h≈g (Setoid.sym B x)) }
7375
}

‎src/Categories/CoYoneda.agda‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,9 @@ module Categories.CoYoneda where
33

44
-- CoYoneda Lemma. See Yoneda for more documentation
55

6-
open import Level
6+
open import Level using (Level; _⊔_; lift; lower)
77
open import Function.Base using (_$_)
88
open import Function.Bundles using (Inverse; Func; _⟨$⟩_)
9-
-- open import Function.Equality using (Π; _⟨$⟩_; cong)
109
open import Relation.Binary.Bundles using (module Setoid)
1110
import Relation.Binary.Reasoning.Setoid as SetoidR
1211
open import Data.Product using (_,_; Σ)
@@ -15,7 +14,7 @@ open import Categories.Category using (Category; _[_,_])
1514
open import Categories.Category.Product using (πʳ; πˡ; _※_)
1615
open import Categories.Category.Construction.Presheaves using (CoPresheaves)
1716
open import Categories.Category.Construction.Functors using (eval)
18-
open import Categories.Category.Construction.Functors
17+
open import Categories.Category.Construction.Functors using (Functors)
1918
open import Categories.Category.Instance.Setoids using (Setoids)
2019
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
2120
open import Categories.Functor.Hom using (module Hom; Hom[_][_,-]; Hom[_][-,-])
@@ -28,6 +27,8 @@ import Categories.Morphism as Mor
2827
import Categories.Morphism.Reasoning as MR
2928
import Categories.NaturalTransformation.Hom as NT-Hom
3029

30+
open Func
31+
3132
private
3233
variable
3334
o ℓ e : Level
@@ -36,7 +37,7 @@ module Yoneda (C : Category o ℓ e) where
3637
open Category C hiding (op) -- uses lots
3738
open HomReasoning using (_○_; ⟺; refl⟩∘⟨_)
3839
open MR C using (id-comm)
39-
open NaturalTransformation
40+
open NaturalTransformation using (η; commute; sym-commute)
4041
open NT-Hom C using (Hom[C,A]⇒Hom[C,B])
4142
private
4243
module CE = Category.Equiv C using (refl)
@@ -76,18 +77,18 @@ module Yoneda (C : Category o ℓ e) where
7677
( λ {b} {nat} eq →
7778
let module SR = SetoidR (F.₀ a) in
7879
let open SR in begin
79-
Func.to (η nat a) id ≈⟨ eq {a} {id} {id} CE.refl ⟩
80-
Func.to (F.₁ id) b ≈⟨ F.identity (Setoid.refl (F.₀ a) {b}) ⟩
80+
to (η nat a) id ≈⟨ eq {a} {id} {id} CE.refl ⟩
81+
to (F.₁ id) b ≈⟨ F.identity (Setoid.refl (F.₀ a) {b}) ⟩
8182
b ∎)
8283
, λ {nat} {y} eq {b} {f} {g} f≈g →
8384
let open Setoid (F.₀ b) in
8485
let module SR = SetoidR (F.₀ b) in
8586
let open SR in
8687
begin
87-
Func.to (F.₁ f) y ≈⟨ Func.cong (F.₁ f) eq ⟩
88-
Func.to (F.₁ f) (Func.to (η nat a) id) ≈⟨ sym-commute nat f CE.refl ⟩
89-
Func.to (η nat b) (f ∘ id ∘ id) ≈⟨ Func.cong (η nat b) (refl⟩∘⟨ identity² ○ (identityʳ ○ f≈g)) ⟩
90-
Func.to (η nat b) g ∎
88+
to (F.₁ f) y ≈⟨ cong (F.₁ f) eq ⟩
89+
to (F.₁ f) (to (η nat a) id) ≈⟨ sym-commute nat f CE.refl ⟩
90+
to (η nat b) (f ∘ id ∘ id) ≈⟨ cong (η nat b) (refl⟩∘⟨ identity² ○ (identityʳ ○ f≈g)) ⟩
91+
to (η nat b) g ∎
9192
}
9293
where
9394
module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity)
@@ -113,7 +114,7 @@ module Yoneda (C : Category o ℓ e) where
113114
; cong = λ i≈j → lift (i≈j CE.refl)
114115
}
115116
; commute = λ where
116-
{_} {G , B} (α , f) {β} {γ} β≈γ → lift $ Func.cong (η α B) (helper f β γ β≈γ)
117+
{_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ)
117118
}
118119
; F⇐G = ntHelper record
119120
{ η = λ (F , A) → record
@@ -134,9 +135,9 @@ module Yoneda (C : Category o ℓ e) where
134135
Setoid._≈_ (Functor.F₀ Nat[Hom[C][c,-],F] (F , A)) β γ →
135136
Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id ∘ f) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id))
136137
helper {F} {A} {B} f β γ β≈γ = S.begin
137-
η β B ⟨$⟩ id ∘ f S.≈⟨ Func.cong (η β B) (MR.id-comm-sym C ○ ∘-resp-≈ʳ (⟺ identity²)) ⟩
138+
η β B ⟨$⟩ id ∘ f S.≈⟨ cong (η β B) (MR.id-comm-sym C ○ ∘-resp-≈ʳ (⟺ identity²)) ⟩
138139
η β B ⟨$⟩ f ∘ id ∘ id S.≈⟨ commute β f CE.refl ⟩
139-
F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ Func.cong (F.₁ f) (β≈γ CE.refl) ⟩
140+
F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩
140141
F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎
141142
where
142143
module F = Functor F using (₀;₁)
@@ -153,9 +154,9 @@ module Yoneda (C : Category o ℓ e) where
153154
Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X)))
154155
(η α Z ⟨$⟩ (Functor.F₁ F (i ∘ f) ⟨$⟩ Y))
155156
helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin
156-
G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ((S′.sym (Func.cong (F.₁ f) eq))) ⟩
157-
η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ Func.cong (η α Z) ((F.F-resp-≈ eq′ S′.refl)) ⟩
158-
η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ Func.cong (η α Z) ((F.homomorphism (Setoid.refl (F.₀ A)))) ⟩
157+
G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X)) S.≈˘⟨ commute α h ((S′.sym (cong (F.₁ f) eq))) ⟩
158+
η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈⟨ cong (η α Z) ((F.F-resp-≈ eq′ S′.refl)) ⟩
159+
η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y)) S.≈˘⟨ cong (η α Z) ((F.homomorphism (Setoid.refl (F.₀ A)))) ⟩
159160
η α Z ⟨$⟩ (F.₁ (i ∘ f) ⟨$⟩ Y) S.∎
160161
where
161162
module F = Functor F using (₀; ₁; homomorphism; F-resp-≈)

‎src/Categories/Functor/Construction/LiftSetoids.agda‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,15 @@
22

33
module Categories.Functor.Construction.LiftSetoids where
44

5-
open import Level
6-
open import Relation.Binary
7-
open import Function.Bundles
5+
open import Level using (Level; _⊔_; Lift; lift)
6+
open import Relation.Binary.Bundles using (Setoid)
7+
open import Function.Bundles using (Func; _⟨$⟩_)
88
open import Function using (_$_) renaming (id to idf)
99

10-
open import Categories.Category
11-
open import Categories.Category.Instance.Setoids
12-
open import Categories.Functor
10+
open import Categories.Category.Instance.Setoids using (Setoids)
11+
open import Categories.Functor.Core using (Functor)
12+
13+
open Func
1314

1415
private
1516
variable
@@ -35,9 +36,9 @@ LiftSetoids c′ ℓ′ = record
3536
{ F₀ = LiftedSetoid c′ ℓ′
3637
; F₁ = λ f → record
3738
{ to = λ where (lift x) → lift $ f ⟨$⟩ x
38-
; cong = λ where (lift eq) → lift $ Func.cong f eq
39+
; cong = λ where (lift eq) → lift $ cong f eq
3940
}
4041
; identity = idf
41-
; homomorphism = λ where {f = f} {g = g} (lift eq) → lift $ Func.cong g $ Func.cong f eq
42+
; homomorphism = λ where {f = f} {g = g} (lift eq) → lift $ cong g $ cong f eq
4243
; F-resp-≈ = λ where fx≈gy (lift x≈y) → lift $ fx≈gy x≈y
4344
}

‎src/Categories/Functor/Construction/ObjectRestriction.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44

55
module Categories.Functor.Construction.ObjectRestriction where
66

7-
open import Level
7+
open import Level using (Level)
88
open import Data.Product using (proj₁; _,_)
99
open import Relation.Unary using (Pred)
1010
open import Function using () renaming (id to id→)
@@ -20,7 +20,7 @@ private
2020
C : Category o ℓ e
2121

2222
RestrictionFunctor : {ℓ′ : Level} → (C : Category o ℓ e) → (E : Pred (Category.Obj C) ℓ′) → Functor (ObjectRestriction C E) C
23-
RestrictionFunctor C E = record
23+
RestrictionFunctor C _ = record
2424
{ F₀ = proj₁
2525
; F₁ = id→
2626
; identity = Equiv.refl

‎src/Categories/Functor/Hom/Properties/Covariant.agda‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,20 @@ open import Categories.Category
44

55
module Categories.Functor.Hom.Properties.Covariant {o ℓ e} (C : Category o ℓ e) where
66

7-
open import Level
7+
open import Level using (Level)
88
open import Function.Bundles using (Func; _⟨$⟩_)
99
open import Relation.Binary using (Setoid)
1010

11-
open import Categories.Category.Construction.Cones
12-
open import Categories.Category.Instance.Setoids
13-
open import Categories.Diagram.Cone.Properties
14-
open import Categories.Diagram.Limit
15-
open import Categories.Functor
16-
open import Categories.Functor.Limits
17-
open import Categories.Functor.Hom
11+
open import Categories.Category.Construction.Cones using (Cone; Cone⇒; Cones)
12+
open import Categories.Category.Instance.Setoids using (Setoids)
13+
open import Categories.Diagram.Cone.Properties using (F-map-Coneˡ)
14+
open import Categories.Diagram.Limit using (Limit; ψ-≈⇒rep-≈)
15+
open import Categories.Functor using (Functor; _∘F_)
16+
open import Categories.Functor.Limits using (Continuous)
17+
open import Categories.Functor.Hom using (module Hom)
1818

1919
import Categories.Morphism.Reasoning as MR
20+
open Func
2021

2122
private
2223
variable

‎src/Categories/Functor/Profunctor/Cograph.agda‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ open import Function.Bundles using (Func; _⟨$⟩_)
1010
open Func using (cong)
1111
open import Relation.Binary using (Setoid; module Setoid)
1212

13-
open import Categories.Category
14-
open import Categories.Functor hiding (id)
13+
open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
14+
open import Categories.Functor using (Functor)
1515
open import Categories.Functor.Bifunctor.Properties using ([_]-commute)
16-
open import Categories.Functor.Profunctor
16+
open import Categories.Functor.Profunctor using (Profunctor)
1717

1818
module _ {o ℓ e o′ ℓ′ e′ ℓ″ e″}
1919
{C : Category o ℓ e} {D : Category o′ ℓ′ e′} (P : Profunctor ℓ″ e″ C D)

‎src/Categories/Functor/Profunctor/FormalComposite.agda‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@
22

33
module Categories.Functor.Profunctor.FormalComposite where
44

5-
open import Level
5+
open import Level using (Level; _⊔_)
6+
open import Relation.Binary.Bundles using (Setoid)
67
open import Relation.Binary.Construct.Closure.SymmetricTransitive as ST using (Plus⇔; minimal)
78
import Relation.Binary.Reasoning.Setoid as SetoidR
89

9-
open import Relation.Binary.Bundles
10-
open import Categories.Category
10+
open import Categories.Category using (Category; _[_,_]; _[_∘_]; _[_≈_])
1111
open import Categories.Category.Instance.Setoids using (Setoids)
12-
open import Categories.Functor hiding (id)
12+
open import Categories.Functor.Core using (Functor)
1313
open import Function.Bundles using (Func; _⟨$⟩_)
1414
open Func using (cong)
1515

‎src/Categories/Functor/Properties.agda‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,10 @@ module Categories.Functor.Properties where
33

44
-- Properties valid of all Functors
55
open import Level using (Level)
6-
open import Data.Product using (proj₁; proj₂; _,_; _×_; Σ)
6+
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
77
open import Function.Base using (_$_)
88
open import Function.Definitions using (Injective; StrictlySurjective)
99
open import Relation.Binary using (_Preserves_⟶_)
10-
open import Relation.Nullary
1110

1211
open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]; module Definitions)
1312
open import Categories.Category.Construction.Core using (module Shorthands)
@@ -47,7 +46,7 @@ EssentiallySurjective {C = C} {D = D} F = (d : Category.Obj D) → Σ C.Obj (λ
4746
module C = Category C
4847

4948
Conservative : Functor C D → Set _
50-
Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (λ h → Iso C f h)
49+
Conservative {C = C} {D = D} F = ∀ {A B} {f : C [ A , B ]} {g : D [ F₀ B , F₀ A ]} → Iso D (F₁ f) g → Σ (C [ B , A ]) (Iso C f)
5150
where
5251
open Functor F
5352
open Morphism

0 commit comments

Comments
 (0)