Proof Assistant Projects
Collection
Digesting proof assistant libraries for AI ingestion. • 103 items • Updated • 3
fact stringlengths 13 12.6k | statement stringlengths 9 8k | proof stringlengths 0 12.1k | type stringclasses 3
values | kind stringclasses 3
values | symbolic_name stringlengths 1 37 | library stringclasses 116
values | filename stringlengths 20 89 | imports listlengths 2 31 | deps listlengths 0 31 | docstring stringclasses 0
values | line_start int64 8 680 | line_end int64 8 680 | has_proof bool 2
classes | source_url stringclasses 1
value | commit stringclasses 1
value | content_level stringclasses 1
value |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
2-Category : (o ℓ e t : Level) → Set (suc (o ⊔ ℓ ⊔ e ⊔ t))
2-Category o ℓ e t = Category (Product.Cats-Monoidal {o} {ℓ} {e}) t | 2-Category : (o ℓ e t : Level) → Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) | 2-Category o ℓ e t = Category (Product.Cats-Monoidal {o} {ℓ} {e}) t | function | definition | 2-Category | Categories | src/Categories/2-Category.agda | [
"Level",
"Categories.Category.Monoidal.Instance.StrictCats",
"Categories.Enriched.Category"
] | [
"Category"
] | null | 10 | 10 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
2-Functor : ∀ {o ℓ e c d} →
2-Category o ℓ e c → 2-Category o ℓ e d → Set (o ⊔ ℓ ⊔ e ⊔ c ⊔ d)
2-Functor C D = Functor (Product.Cats-Monoidal) C D | 2-Functor : ∀ {o ℓ e c d} →
2-Category o ℓ e c → 2-Category o ℓ e d → Set (o ⊔ ℓ ⊔ e ⊔ c ⊔ d) | 2-Functor C D = Functor (Product.Cats-Monoidal) C D | function | definition | 2-Functor | Categories | src/Categories/2-Functor.agda | [
"Level",
"Categories.Category.Monoidal.Instance.StrictCats",
"Categories.2-Category",
"Categories.Enriched.Functor"
] | [
"2-Category",
"Functor"
] | null | 11 | 12 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
private
module C = Category C
module D = Category D
module L = Functor L
module R = Functor R
field
unit : NaturalTransformation idF (R ∘F L)
counit : NaturalTransformation (L ∘F R) idF
modul... | record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
private
module C = Category C
module D = Category D
module L = Functor L
module R = Functor R
field
unit : NaturalTransformation idF (R ∘F L)
counit : NaturalTransformation (L ∘F R) idF
modul... | record | structure | Adjoint | Categories | src/Categories/Adjoint.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Relation.Binary.PropositionalEquality",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom"... | [
"B",
"Bifunctor",
"Category",
"Functor",
"Hom",
"Inverse",
"L",
"LiftSetoids",
"NaturalIsomorphism",
"NaturalTransformation",
"Setoids",
"X",
"_",
"f",
"g",
"ntHelper",
"op",
"η"
] | null | 33 | 203 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
⊣-id : idF {C = C} ⊣ idF {C = C}
⊣-id {C = C} = record
{ unit = F⇐G unitorˡ
; counit = F⇒G unitorʳ
; zig = identityˡ
; zag = identityʳ
}
where open Category C
open NaturalIsomorphism | ⊣-id : idF {C = C} ⊣ idF {C = C} | ⊣-id {C = C} = record
{ unit = F⇐G unitorˡ
; counit = F⇒G unitorʳ
; zig = identityˡ
; zag = identityʳ
}
where open Category C
open NaturalIsomorphism | function | definition | ⊣-id | Categories | src/Categories/Adjoint.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Relation.Binary.PropositionalEquality",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom"... | [
"Category",
"NaturalIsomorphism",
"unitorʳ",
"unitorˡ"
] | null | 208 | 208 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
private
op-involutive : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) →
Adjoint.op (Adjoint.op L⊣R) ≡ L⊣R
op-involutive _ = ≡.refl | private
op-involutive : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D} {R : Functor D C} (L⊣R : L ⊣ R) →
Adjoint.op (Adjoint.op L⊣R) ≡ L⊣R
op-involutive _ = ≡.refl | function | definition | op-involutive | Categories | src/Categories/Adjoint.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Relation.Binary.PropositionalEquality",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom"... | [
"Category",
"Functor",
"L",
"_"
] | null | 218 | 221 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
_⊣_ = Adjoint | _⊣_ = Adjoint | function | definition | _⊣_ | Categories | src/Categories/Adjoint.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Relation.Binary.PropositionalEquality",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom"... | [
"Adjoint"
] | null | 206 | 206 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where
field
enriched : Enriched (Product.Cats-Monoidal {o} {ℓ} {e}) t
open Enriched enriched public
module hom {A B} = Category (hom A B)
module ComHom {A B} = Commutation (hom A B)
infix 4 _⇒₁_ _⇒₂_ _≈_
infixr 7 _∘ᵥ_ _∘₁_
infixr 9 _▷_
infixl 9... | record Bicategory o ℓ e t : Set (suc (o ⊔ ℓ ⊔ e ⊔ t)) where
field
enriched : Enriched (Product.Cats-Monoidal {o} {ℓ} {e}) t
open Enriched enriched public
module hom {A B} = Category (hom A B)
module ComHom {A B} = Commutation (hom A B)
infix 4 _⇒₁_ _⇒₂_ _≈_
infixr 7 _∘ᵥ_ _∘₁_
infixr 9 _▷_
infixl 9... | record | structure | Bicategory | Categories | src/Categories/Bicategory.agda | [
"Level",
"Data.Product",
"Relation.Binary",
"Categories.Category",
"Categories.Category.Monoidal.Instance.Cats",
"Categories.Enriched.Category",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism"
] | [
"B",
"Category",
"_",
"_∘ᵥ_",
"_∘ₕ_",
"_≈_",
"f",
"g",
"id",
"pentagon",
"triangle",
"α",
"λ⇒",
"⊚"
] | null | 17 | 97 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
_[_,_] : (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ
_[_,_] = Category._⇒_
_[_≈_] = Category._≈_
_[_∘_] = Category._∘_ | _[_,_] : (C : Category o ℓ e) → (X : Category.Obj C) → (Y : Category.Obj C) → Set ℓ | _[_,_] = Category._⇒_
_[_≈_] = Category._≈_
_[_∘_] = Category._∘_ | function | definition | _ | Categories | src/Categories/Category.agda | [
"Level",
"Categories.Category.Core"
] | [
"Category",
"X",
"_∘_",
"_≈_"
] | null | 19 | 19 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record Comonad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
field
F : Endofunctor C
ε : NaturalTransformation F idF
δ : NaturalTransformation F (F ∘F F)
module F = Functor F
module ε = NaturalTransformation ε
module δ = NaturalTransformation δ
open Category C
open Functor F
field
... | record Comonad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
field
F : Endofunctor C
ε : NaturalTransformation F idF
δ : NaturalTransformation F (F ∘F F)
module F = Functor F
module ε = NaturalTransformation ε
module δ = NaturalTransformation δ
open Category C
open Functor F
field
... | record | structure | Comonad | Categories | src/Categories/Comonad.agda | [
"Level",
"Categories.Category",
"Categories.Functor",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Equivalence"
] | [
"Category",
"Endofunctor",
"F",
"Functor",
"NaturalTransformation",
"X",
"id"
] | null | 13 | 30 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
Endofunctor : Category o ℓ e → Set _
Endofunctor C = Functor C C | Endofunctor : Category o ℓ e → Set _ | Endofunctor C = Functor C C | function | definition | Endofunctor | Categories | src/Categories/Functor.agda | [
"Level",
"Function",
"Categories.Category",
"Categories.Functor.Core"
] | [
"Category",
"Functor",
"_"
] | null | 14 | 14 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
id : ∀ {C : Category o ℓ e} → Functor C C
id {C = C} = record
{ F₀ = id→
; F₁ = id→
; identity = Category.Equiv.refl C
; homomorphism = Category.Equiv.refl C
; F-resp-≈ = id→
} | id : ∀ {C : Category o ℓ e} → Functor C C | id {C = C} = record
{ F₀ = id→
; F₁ = id→
; identity = Category.Equiv.refl C
; homomorphism = Category.Equiv.refl C
; F-resp-≈ = id→
} | function | definition | id | Categories | src/Categories/Functor.agda | [
"Level",
"Function",
"Categories.Category",
"Categories.Functor.Core"
] | [
"Category",
"Functor",
"identity"
] | null | 17 | 17 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
_∘F_ : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o″ ℓ″ e″}
→ Functor D E → Functor C D → Functor C E
_∘F_ {C = C} {D = D} {E = E} F G = record
{ F₀ = F.₀ ● G.₀
; F₁ = F.₁ ● G.₁
; identity = identity′
; homomorphism = homomorphism′
; F-resp-≈ = F.F-resp-≈ ● G.F-resp-≈
}
where
modu... | _∘F_ : ∀ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o″ ℓ″ e″}
→ Functor D E → Functor C D → Functor C E | _∘F_ {C = C} {D = D} {E = E} F G = record
{ F₀ = F.₀ ● G.₀
; F₁ = F.₁ ● G.₁
; identity = identity′
; homomorphism = homomorphism′
; F-resp-≈ = F.F-resp-≈ ● G.F-resp-≈
}
where
module C = Category C using (id)
module D = Category D using (id)
module E = Category E using (id; module HomReasoning)
mo... | function | definition | _∘F_ | Categories | src/Categories/Functor.agda | [
"Level",
"Function",
"Categories.Category",
"Categories.Functor.Core"
] | [
"Category",
"F",
"Functor",
"X",
"f",
"g",
"id",
"identity"
] | null | 30 | 31 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
GlobularSet : (o : Level) → Set (suc o)
GlobularSet o = Presheaf Globe (Sets o)
-- TODO? make universe polymorphic with polymorphic ⊤ | GlobularSet : (o : Level) → Set (suc o) | GlobularSet o = Presheaf Globe (Sets o)
-- TODO? make universe polymorphic with polymorphic ⊤ | function | definition | GlobularSet | Categories | src/Categories/GlobularSet.agda | [
"Level",
"Data.Unit",
"Relation.Binary.PropositionalEquality",
"Categories.Category",
"Categories.Category.Instance.Globe",
"Categories.Category.Instance.Sets",
"Categories.Functor",
"Categories.Functor.Presheaf"
] | [
"Globe",
"Presheaf",
"Sets"
] | null | 21 | 21 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Trivial : GlobularSet zero
Trivial = record
{ F₀ = λ _ → ⊤
; F₁ = λ _ x → x
; identity = λ _ → refl
; homomorphism = λ _ → refl
; F-resp-≈ = λ _ _ → refl
} | Trivial : GlobularSet zero | Trivial = record
{ F₀ = λ _ → ⊤
; F₁ = λ _ x → x
; identity = λ _ → refl
; homomorphism = λ _ → refl
; F-resp-≈ = λ _ _ → refl
} | function | definition | Trivial | Categories | src/Categories/GlobularSet.agda | [
"Level",
"Data.Unit",
"Relation.Binary.PropositionalEquality",
"Categories.Category",
"Categories.Category.Instance.Globe",
"Categories.Category.Instance.Sets",
"Categories.Functor",
"Categories.Functor.Presheaf"
] | [
"GlobularSet",
"_",
"identity",
"refl",
"x"
] | null | 25 | 25 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
GlobularObject : Category o ℓ e → Set _
GlobularObject C = Functor (Category.op Globe) C | GlobularObject : Category o ℓ e → Set _ | GlobularObject C = Functor (Category.op Globe) C | function | definition | GlobularObject | Categories | src/Categories/GlobularSet.agda | [
"Level",
"Data.Unit",
"Relation.Binary.PropositionalEquality",
"Categories.Category",
"Categories.Category.Instance.Globe",
"Categories.Category.Instance.Sets",
"Categories.Functor",
"Categories.Functor.Presheaf"
] | [
"Category",
"Functor",
"Globe",
"_"
] | null | 34 | 34 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record -2-Category : Set (suc (o ⊔ ℓ ⊔ e)) where
field
cat : Category o ℓ e
open Category cat public
open M cat using (_≅_)
field
Obj-Contr : Σ Obj (λ x → (y : Obj) → x ≅ y)
Hom-Conn : {x y : Obj} {f g : x ⇒ y} → f ≈ g | record -2-Category : Set (suc (o ⊔ ℓ ⊔ e)) where
field
cat : Category o ℓ e
open Category cat public
open M cat using (_≅_)
field
Obj-Contr : Σ Obj (λ x → (y : Obj) → x ≅ y)
Hom-Conn : {x y : Obj} {f g : x ⇒ y} → f ≈ g | record | structure | -2-Category | Categories | src/Categories/Minus2-Category.agda | [
"Level",
"Categories.Category",
"Data.Product",
"Categories.Morphism"
] | [
"Category",
"_≅_",
"f",
"g",
"x"
] | null | 29 | 37 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
field
F : Endofunctor C
η : NaturalTransformation idF F
μ : NaturalTransformation (F ∘F F) F
module F = Functor F
module η = NaturalTransformation η
module μ = NaturalTransformation μ
open Category C
open F
field
assoc ... | record Monad {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
field
F : Endofunctor C
η : NaturalTransformation idF F
μ : NaturalTransformation (F ∘F F) F
module F = Functor F
module η = NaturalTransformation η
module μ = NaturalTransformation μ
open Category C
open F
field
assoc ... | record | structure | Monad | Categories | src/Categories/Monad.agda | [
"Level",
"Categories.Category",
"Categories.Functor",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Equivalence"
] | [
"Category",
"Endofunctor",
"F",
"Functor",
"NaturalTransformation",
"X",
"id",
"η"
] | null | 13 | 30 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record _↣_ (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
mor : A ⇒ B
mono : Mono mor | record _↣_ (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
mor : A ⇒ B
mono : Mono mor | record | structure | _↣_ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Mono",
"mono"
] | null | 35 | 38 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record _↠_ (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
mor : A ⇒ B
epi : Epi mor | record _↠_ (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where
field
mor : A ⇒ B
epi : Epi mor | record | structure | _↠_ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Epi",
"epi"
] | null | 49 | 52 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record Retract (X U : Obj) : Set (ℓ ⊔ e) where
field
section : X ⇒ U
retract : U ⇒ X
is-retract : retract ∘ section ≈ id | record Retract (X U : Obj) : Set (ℓ ⊔ e) where
field
section : X ⇒ U
retract : U ⇒ X
is-retract : retract ∘ section ≈ id | record | structure | Retract | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"X",
"id"
] | null | 60 | 64 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record Iso (from : A ⇒ B) (to : B ⇒ A) : Set e where
field
isoˡ : to ∘ from ≈ id
isoʳ : from ∘ to ≈ id
-- We often say that a morphism "is an iso" if there exists some inverse to it.
-- This does buck the naming convention we use somewhat, but it lines up
-- better with the literature. | record Iso (from : A ⇒ B) (to : B ⇒ A) : Set e where
field
isoˡ : to ∘ from ≈ id
isoʳ : from ∘ to ≈ id
-- We often say that a morphism "is an iso" if there exists some inverse to it.
-- This does buck the naming convention we use somewhat, but it lines up
-- better with the literature. | record | structure | Iso | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"id"
] | null | 66 | 73 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record IsIso (from : A ⇒ B) : Set (ℓ ⊔ e) where
field
inv : B ⇒ A
iso : Iso from inv
open Iso iso public | record IsIso (from : A ⇒ B) : Set (ℓ ⊔ e) where
field
inv : B ⇒ A
iso : Iso from inv
open Iso iso public | record | structure | IsIso | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Iso"
] | null | 74 | 79 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record _≅_ (A B : Obj) : Set (ℓ ⊔ e) where
field
from : A ⇒ B
to : B ⇒ A
iso : Iso from to
open Iso iso public
-- don't pollute the name space too much | record _≅_ (A B : Obj) : Set (ℓ ⊔ e) where
field
from : A ⇒ B
to : B ⇒ A
iso : Iso from to
open Iso iso public
-- don't pollute the name space too much | record | structure | _≅_ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Iso"
] | null | 82 | 90 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
Mono : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
Mono {A = A} f = ∀ {C} → (g₁ g₂ : C ⇒ A) → f ∘ g₁ ≈ f ∘ g₂ → g₁ ≈ g₂ | Mono : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e) | Mono {A = A} f = ∀ {C} → (g₁ g₂ : C ⇒ A) → f ∘ g₁ ≈ f ∘ g₂ → g₁ ≈ g₂ | function | definition | Mono | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f"
] | null | 26 | 26 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
JointMono : {ι : Level} (I : Set ι) (B : I → Obj) → ((i : I) → A ⇒ B i) → Set (o ⊔ ℓ ⊔ e ⊔ ι)
JointMono {A} I B f = ∀ {C} → (g₁ g₂ : C ⇒ A) → ((i : I) → f i ∘ g₁ ≈ f i ∘ g₂) → g₁ ≈ g₂ | JointMono : {ι : Level} (I : Set ι) (B : I → Obj) → ((i : I) → A ⇒ B i) → Set (o ⊔ ℓ ⊔ e ⊔ ι) | JointMono {A} I B f = ∀ {C} → (g₁ g₂ : C ⇒ A) → ((i : I) → f i ∘ g₁ ≈ f i ∘ g₂) → g₁ ≈ g₂ | function | definition | JointMono | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f"
] | null | 29 | 29 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
JointMono₂ : (f : A ⇒ B) (g : A ⇒ C) → Set (o ⊔ ℓ ⊔ e)
JointMono₂ {A}{B}{C} f g = JointMono (Fin 2) (λ{zero → B; (nzero _) → C}) (λ{zero → f; (nzero _) → g}) | JointMono₂ : (f : A ⇒ B) (g : A ⇒ C) → Set (o ⊔ ℓ ⊔ e) | JointMono₂ {A}{B}{C} f g = JointMono (Fin 2) (λ{zero → B; (nzero _) → C}) (λ{zero → f; (nzero _) → g}) | function | definition | JointMono₂ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Fin",
"JointMono",
"_",
"f",
"g"
] | null | 32 | 32 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Epi : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e)
Epi {B = B} f = ∀ {C} → (g₁ g₂ : B ⇒ C) → g₁ ∘ f ≈ g₂ ∘ f → g₁ ≈ g₂ | Epi : ∀ (f : A ⇒ B) → Set (o ⊔ ℓ ⊔ e) | Epi {B = B} f = ∀ {C} → (g₁ g₂ : B ⇒ C) → g₁ ∘ f ≈ g₂ ∘ f → g₁ ≈ g₂ | function | definition | Epi | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f"
] | null | 40 | 40 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
JointEpi : (I : Set) (A : I → Obj) → ((i : I) → A i ⇒ B) → Set (o ⊔ ℓ ⊔ e)
JointEpi {B} I A f = ∀ {C} → (g₁ g₂ : B ⇒ C) → ((i : I) → g₁ ∘ f i ≈ g₂ ∘ f i) → g₁ ≈ g₂ | JointEpi : (I : Set) (A : I → Obj) → ((i : I) → A i ⇒ B) → Set (o ⊔ ℓ ⊔ e) | JointEpi {B} I A f = ∀ {C} → (g₁ g₂ : B ⇒ C) → ((i : I) → g₁ ∘ f i ≈ g₂ ∘ f i) → g₁ ≈ g₂ | function | definition | JointEpi | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f"
] | null | 43 | 43 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
JointEpi₂ : (f : A ⇒ B) (g : C ⇒ B) → Set (o ⊔ ℓ ⊔ e)
JointEpi₂ {A}{B}{C} f g = JointEpi (Fin 2) (λ{zero → A; (nzero _) → C}) (λ{zero → f; (nzero _) → g}) | JointEpi₂ : (f : A ⇒ B) (g : C ⇒ B) → Set (o ⊔ ℓ ⊔ e) | JointEpi₂ {A}{B}{C} f g = JointEpi (Fin 2) (λ{zero → A; (nzero _) → C}) (λ{zero → f; (nzero _) → g}) | function | definition | JointEpi₂ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"Fin",
"JointEpi",
"_",
"f",
"g"
] | null | 46 | 46 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
_SectionOf_ : (g : B ⇒ A) (f : A ⇒ B) → Set e | _SectionOf_ : (g : B ⇒ A) (f : A ⇒ B) → Set e | function | definition | _SectionOf_ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f",
"g"
] | null | 54 | 54 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
_RetractOf_ : (g : B ⇒ A) (f : A ⇒ B) → Set e | _RetractOf_ : (g : B ⇒ A) (f : A ⇒ B) → Set e | function | definition | _RetractOf_ | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"B",
"f",
"g"
] | null | 57 | 57 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
private
≅-refl : Reflexive _≅_
≅-refl = record
{ from = id
; to = id
; iso = record
{ isoˡ = identity²
; isoʳ = identity²
}
}
≅-sym : Symmetric _≅_
≅-sym A≅B = record
{ from = to
; to = from
; iso = record
{ isoˡ = isoʳ
; isoʳ = isoˡ
}
}... | private
≅-refl : Reflexive _≅_
≅-refl = record
{ from = id
; to = id
; iso = record
{ isoˡ = identity²
; isoʳ = identity²
}
}
≅-sym : Symmetric _≅_
≅-sym A≅B = record
{ from = to
; to = from
; iso = record
{ isoˡ = isoʳ
; isoʳ = isoˡ
}
}... | function | definition | ≅-refl | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"Symmetric",
"_≅_",
"id"
] | null | 91 | 130 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
≅-isEquivalence : IsEquivalence _≅_
≅-isEquivalence = record
{ refl = ≅-refl
; sym = ≅-sym
; trans = ≅-trans
}
-- But make accessing it easy: | ≅-isEquivalence : IsEquivalence _≅_ | ≅-isEquivalence = record
{ refl = ≅-refl
; sym = ≅-sym
; trans = ≅-trans
}
-- But make accessing it easy: | function | definition | ≅-isEquivalence | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"_≅_",
"refl",
"sym",
"trans",
"≅-refl"
] | null | 132 | 132 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
≅-setoid : Setoid _ _
≅-setoid = record
{ Carrier = Obj
; _≈_ = _≅_
; isEquivalence = ≅-isEquivalence
} | ≅-setoid : Setoid _ _ | ≅-setoid = record
{ Carrier = Obj
; _≈_ = _≅_
; isEquivalence = ≅-isEquivalence
} | function | definition | ≅-setoid | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"_",
"_≅_",
"_≈_",
"isEquivalence",
"≅-isEquivalence"
] | null | 142 | 142 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
g SectionOf f = f ∘ g ≈ id
g RetractOf f = g ∘ f ≈ id | g SectionOf f = f ∘ g ≈ id | g RetractOf f = g ∘ f ≈ id | function | definition | g | Categories | src/Categories/Morphism.agda | [
"Categories.Category.Core",
"Level",
"Relation.Binary",
"Data.Fin",
"Categories.Morphism.Reasoning.Core"
] | [
"f",
"id"
] | null | 55 | 55 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record Pseudofunctor : Set (o ⊔ ℓ ⊔ e ⊔ t ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ t′) where
field
P₀ : C.Obj → D.Obj
P₁ : {x y : C.Obj} → Functor (C.hom x y) (D.hom (P₀ x) (P₀ y))
-- For maximal generality, shift the levels of One. P preserves id
P-identity : {A : C.Obj} → D.id {P₀ A} ∘F shift o′ ℓ′ e′ ≃ P₁ ∘F (C.id {A})
... | record Pseudofunctor : Set (o ⊔ ℓ ⊔ e ⊔ t ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ t′) where
field
P₀ : C.Obj → D.Obj
P₁ : {x y : C.Obj} → Functor (C.hom x y) (D.hom (P₀ x) (P₀ y))
-- For maximal generality, shift the levels of One. P preserves id
P-identity : {A : C.Obj} → D.id {P₀ A} ∘F shift o′ ℓ′ e′ ≃ P₁ ∘F (C.id {A})
... | record | structure | Pseudofunctor | Categories | src/Categories/Pseudofunctor.agda | [
"Categories.Bicategory",
"Level",
"Data.Product",
"Categories.Bicategory.Extras",
"Categories.Category",
"Categories.Category.Instance.One",
"Categories.Category.Product",
"Categories.Functor",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism"
] | [
"Functor",
"Hom",
"NaturalTransformation",
"_",
"f",
"g",
"id",
"shift",
"x",
"α"
] | null | 35 | 94 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
_∘⊣_ : {L : Functor C D} {R : Functor D C} {M : Functor D E} {S : Functor E D} →
L ⊣ R → M ⊣ S → (M ∘F L) ⊣ (R ∘F S)
_∘⊣_ {C = C} {D = D} {E = E} {L = L} {R} {M} {S} LR MS = record
{ unit = ((F⇐G (associator _ S R) ∘ᵥ R ∘ˡ (F⇒G (associator L M S))) ∘ᵥ
(R ∘ˡ (MSη′ ∘ʳ L)) ∘ᵥ (R ∘ˡ (F⇐G unitorˡ))) ∘ᵥ LRη′... | _∘⊣_ : {L : Functor C D} {R : Functor D C} {M : Functor D E} {S : Functor E D} →
L ⊣ R → M ⊣ S → (M ∘F L) ⊣ (R ∘F S) | _∘⊣_ {C = C} {D = D} {E = E} {L = L} {R} {M} {S} LR MS = record
{ unit = ((F⇐G (associator _ S R) ∘ᵥ R ∘ˡ (F⇒G (associator L M S))) ∘ᵥ
(R ∘ˡ (MSη′ ∘ʳ L)) ∘ᵥ (R ∘ˡ (F⇐G unitorˡ))) ∘ᵥ LRη′
; counit = MSε′ ∘ᵥ (((F⇒G (unitorʳ {F = M}) ∘ʳ S) ∘ᵥ ((M ∘ˡ LRε′) ∘ʳ S)) ∘ᵥ
(F⇒G (associator R L M) ∘ʳ ... | function | definition | _∘⊣_ | Categories.Adjoint | src/Categories/Adjoint/Compose.agda | [
"Level",
"Data.Product",
"Function",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Morphism",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom",
"Categories.... | [
"Adjoint",
"B",
"Category",
"F",
"Functor",
"L",
"NaturalIsomorphism",
"NaturalTransformation",
"_",
"_∘_",
"_≈_",
"_⊚_",
"associator",
"id",
"identity",
"unitorʳ",
"unitorˡ",
"η",
"⊚"
] | null | 35 | 36 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record ⊣Equivalence (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
field
L : Functor C D
R : Functor D C
L⊣⊢R : L ⊣⊢ R
module L = Functor L
module R = Functor R
open _⊣⊢_ L⊣⊢R public | record ⊣Equivalence (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
field
L : Functor C D
R : Functor D C
L⊣⊢R : L ⊣⊢ R
module L = Functor L
module R = Functor R
open _⊣⊢_ L⊣⊢R public | record | structure | ⊣Equivalence | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"Category",
"Functor",
"L",
"_⊣⊢_"
] | null | 21 | 30 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
refl : ⊣Equivalence C C
refl = record
{ L = idF
; R = idF
; L⊣⊢R = id⊣⊢id
} | refl : ⊣Equivalence C C | refl = record
{ L = idF
; R = idF
; L⊣⊢R = id⊣⊢id
} | function | definition | refl | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"L",
"id⊣⊢id",
"⊣Equivalence"
] | null | 32 | 32 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
sym : ⊣Equivalence C D → ⊣Equivalence D C
sym e = record
{ L = R
; R = L
; L⊣⊢R = op₂
}
where open ⊣Equivalence e | sym : ⊣Equivalence C D → ⊣Equivalence D C | sym e = record
{ L = R
; R = L
; L⊣⊢R = op₂
}
where open ⊣Equivalence e | function | definition | sym | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"L",
"⊣Equivalence"
] | null | 39 | 39 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
trans : ⊣Equivalence C D → ⊣Equivalence D E → ⊣Equivalence C E
trans e e′ = record
{ L = e′.L ∘F e.L
; R = e.R ∘F e′.R
; L⊣⊢R = e.L⊣⊢R ∘⊣⊢ e′.L⊣⊢R
}
where module e = ⊣Equivalence e using (L; R; L⊣⊢R)
module e′ = ⊣Equivalence e′ using (L; R; L⊣⊢R) | trans : ⊣Equivalence C D → ⊣Equivalence D E → ⊣Equivalence C E | trans e e′ = record
{ L = e′.L ∘F e.L
; R = e.R ∘F e′.R
; L⊣⊢R = e.L⊣⊢R ∘⊣⊢ e′.L⊣⊢R
}
where module e = ⊣Equivalence e using (L; R; L⊣⊢R)
module e′ = ⊣Equivalence e′ using (L; R; L⊣⊢R) | function | definition | trans | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"L",
"⊣Equivalence"
] | null | 47 | 47 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
isEquivalence : ∀ {o ℓ e} → IsEquivalence (⊣Equivalence {o} {ℓ} {e})
isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
} | isEquivalence : ∀ {o ℓ e} → IsEquivalence (⊣Equivalence {o} {ℓ} {e}) | isEquivalence = record
{ refl = refl
; sym = sym
; trans = trans
} | function | definition | isEquivalence | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"refl",
"sym",
"trans",
"⊣Equivalence"
] | null | 56 | 56 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
setoid : ∀ o ℓ e → Setoid _ _
setoid o ℓ e = record
{ Carrier = Category o ℓ e
; _≈_ = ⊣Equivalence
; isEquivalence = isEquivalence
} | setoid : ∀ o ℓ e → Setoid _ _ | setoid o ℓ e = record
{ Carrier = Category o ℓ e
; _≈_ = ⊣Equivalence
; isEquivalence = isEquivalence
} | function | definition | setoid | Categories.Adjoint | src/Categories/Adjoint/Equivalence.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.TwoSided",
"Categories.Adjoint.TwoSided.Compose",
"Categories.Category.Core",
"Categories.Functor",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Relation.Binary"
] | [
"Category",
"_",
"_≈_",
"isEquivalence",
"⊣Equivalence"
] | null | 63 | 63 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record Mate {L : Functor C D}
(L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′)
(α : NaturalTransformation L L′)
(β : NaturalTransformation R′ R) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
private
module L⊣R = Adjoint L⊣R
module L′⊣R′ = Adjoint L′⊣R′
module C = Category C
mo... | record Mate {L : Functor C D}
(L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′)
(α : NaturalTransformation L L′)
(β : NaturalTransformation R′ R) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
private
module L⊣R = Adjoint L⊣R
module L′⊣R′ = Adjoint L′⊣R′
module C = Category C
mo... | record | structure | Mate | Categories.Adjoint | src/Categories/Adjoint/Mate.agda | [
"Level",
"Data.Product",
"Function.Bundles",
"Function.Construct.Composition",
"Function.Construct.Setoid",
"Relation.Binary",
"Categories.Category",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Hom",
"Categories.NaturalTransformation",
"Categories.NaturalT... | [
"Adjoint",
"Category",
"Functor",
"L",
"NaturalTransformation",
"X",
"_",
"α",
"η"
] | null | 32 | 79 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record HaveMate {L L′ : Functor C D} {R R′ : Functor D C}
(L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
field
α : NaturalTransformation L L′
β : NaturalTransformation R′ R
mate : Mate L⊣R L′⊣R′ α β
module α = NaturalTransformation α
module β =... | record HaveMate {L L′ : Functor C D} {R R′ : Functor D C}
(L⊣R : L ⊣ R) (L′⊣R′ : L′ ⊣ R′) : Set (levelOfTerm L⊣R ⊔ levelOfTerm L′⊣R′) where
field
α : NaturalTransformation L L′
β : NaturalTransformation R′ R
mate : Mate L⊣R L′⊣R′ α β
module α = NaturalTransformation α
module β =... | record | structure | HaveMate | Categories.Adjoint | src/Categories/Adjoint/Mate.agda | [
"Level",
"Data.Product",
"Function.Bundles",
"Function.Construct.Composition",
"Function.Construct.Setoid",
"Relation.Binary",
"Categories.Category",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Hom",
"Categories.NaturalTransformation",
"Categories.NaturalT... | [
"Functor",
"L",
"Mate",
"NaturalTransformation",
"α"
] | null | 81 | 94 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
private
T : Monad 𝒞
T = adjoint⇒monad adjoint
field
Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟
comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹ | record IsMonadicAdjunction {L : Functor 𝒞 𝒟} {R : Functor 𝒟 𝒞} (adjoint : L ⊣ R) : Set (levelOfTerm 𝒞 ⊔ levelOfTerm 𝒟) where
private
T : Monad 𝒞
T = adjoint⇒monad adjoint
field
Comparison⁻¹ : Functor (EilenbergMoore T) 𝒟
comparison-equiv : WeakInverse (ComparisonF adjoint) Comparison⁻¹ | record | structure | IsMonadicAdjunction | Categories.Adjoint | src/Categories/Adjoint/Monadic.agda | [
"Level",
"Categories.Adjoint",
"Categories.Adjoint.Properties",
"Categories.Category",
"Categories.Category.Equivalence",
"Categories.Functor",
"Categories.Monad",
"Categories.Category.Construction.EilenbergMoore",
"Categories.Category.Construction.Properties.EilenbergMoore"
] | [
"EilenbergMoore",
"Functor",
"L",
"Monad",
"WeakInverse",
"𝒞"
] | null | 25 | 32 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E)) (R : Functor (Category.op C) (Functors E D)) : Set (o ⊔ ℓ ⊔ e) where
private
module C = Category C
module D = Category D
module E = Category E
module L = Functor L
module R = Functor R
-- use double letters whenev... | record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E)) (R : Functor (Category.op C) (Functors E D)) : Set (o ⊔ ℓ ⊔ e) where
private
module C = Category C
module D = Category D
module E = Category E
module L = Functor L
module R = Functor R
-- use double letters whenev... | record | structure | ParametricAdjoint | Categories.Adjoint | src/Categories/Adjoint/Parametric.agda | [
"Level",
"Data.Product",
"Function.Bundles",
"Function.Properties.Inverse",
"Categories.Category.Core",
"Categories.Functor",
"Categories.Adjoint",
"Categories.Category.Construction.Functors",
"Categories.Diagram.Cowedge",
"Categories.NaturalTransformation.Dinatural",
"Categories.Functor.Bifunct... | [
"Adjoint",
"Bifunctor",
"Category",
"Cowedge",
"DinaturalTransformation",
"F",
"Functor",
"Functors",
"L",
"X",
"_",
"const",
"dtHelper",
"f",
"g",
"identity",
"x",
"α",
"η"
] | null | 28 | 144 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
ra-preserves-diagram : {L : Functor J K} {R : Functor K J} (L⊣R : L ⊣ R) {F : Functor J C} → Colimit F → Colimit (F ∘F R)
ra-preserves-diagram L⊣R colim = Duality.coLimit⇒Colimit _ (la-preserves-diagram (Adjoint.op L⊣R) (Duality.Colimit⇒coLimit _ colim))
-- adjoint functors induce monads and comonads | ra-preserves-diagram : {L : Functor J K} {R : Functor K J} (L⊣R : L ⊣ R) {F : Functor J C} → Colimit F → Colimit (F ∘F R) | ra-preserves-diagram L⊣R colim = Duality.coLimit⇒Colimit _ (la-preserves-diagram (Adjoint.op L⊣R) (Duality.Colimit⇒coLimit _ colim))
-- adjoint functors induce monads and comonads | function | definition | ra-preserves-diagram | Categories.Adjoint | src/Categories/Adjoint/Properties.agda | [
"Level",
"Data.Product",
"Function.Base",
"Categories.Adjoint",
"Categories.Adjoint.Equivalents",
"Categories.Adjoint.RAPL",
"Categories.Category",
"Categories.Category.Product",
"Categories.Category.Construction.Comma",
"Categories.Diagram.Cone",
"Categories.Diagram.Cone.Properties",
"Categor... | [
"Colimit",
"F",
"Functor",
"L",
"_"
] | null | 238 | 238 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record RelativeAdjoint {C : Category o ℓ e} (D : Category o ℓ e) (J : Functor E C) : Set (levelOfTerm D ⊔ levelOfTerm J) where
field
L : Functor E D
R : Functor D C
private
module C = Category C
module D = Category D
module E = Category E
module L = Functor L
module R = Functor R
m... | record RelativeAdjoint {C : Category o ℓ e} (D : Category o ℓ e) (J : Functor E C) : Set (levelOfTerm D ⊔ levelOfTerm J) where
field
L : Functor E D
R : Functor D C
private
module C = Category C
module D = Category D
module E = Category E
module L = Functor L
module R = Functor R
m... | record | structure | RelativeAdjoint | Categories.Adjoint | src/Categories/Adjoint/Relative.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom",
"Categories.Nat... | [
"Bifunctor",
"Category",
"Functor",
"Hom",
"L",
"NaturalIsomorphism",
"Setoids",
"_"
] | null | 38 | 61 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
RA⇒RMonad : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} {J : Functor E C} → RelativeAdjoint D J → RMonad J
RA⇒RMonad {C = C} {D} {E} {J} RA = record
{ F₀ = F₀ (R ∘F L)
; unit = λ {c} → ⇐.η (c , F₀ L c) ⟨$⟩ D.id {F₀ L c}
; extend = λ {X} {Y} k → F₁ R (⇒.η (X , F₀ L Y) ⟨$⟩ k)
; identityʳ = idʳ
; identityˡ = ... | RA⇒RMonad : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} {J : Functor E C} → RelativeAdjoint D J → RMonad J | RA⇒RMonad {C = C} {D} {E} {J} RA = record
{ F₀ = F₀ (R ∘F L)
; unit = λ {c} → ⇐.η (c , F₀ L c) ⟨$⟩ D.id {F₀ L c}
; extend = λ {X} {Y} k → F₁ R (⇒.η (X , F₀ L Y) ⟨$⟩ k)
; identityʳ = idʳ
; identityˡ = R.F-resp-≈ (iso.isoʳ _) ○ R.identity
; assoc = a
; sym-assoc = sym a
; extend-≈ = λ k≈h → F-resp-≈ R (Fu... | function | definition | RA⇒RMonad | Categories.Adjoint | src/Categories/Adjoint/Relative.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom",
"Categories.Nat... | [
"Category",
"Functor",
"L",
"NaturalIsomorphism",
"RelativeAdjoint",
"X",
"_",
"sym",
"x"
] | null | 63 | 63 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
⊣⇒RAdjoint : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} (L : Functor C D) (R : Functor D C) (J : Functor E C) → L ⊣ R → RelativeAdjoint D J
⊣⇒RAdjoint {C = C} {D} L R J A = record
{ L = L ∘F J
; R = R
; Hom-NI = record
{ F⇒G = ntHelper record
{ η = λ _ → record { to = Radjunct ; cong = ∘-resp-≈ʳ ∙ L... | ⊣⇒RAdjoint : {C D : Category o ℓ e} {E : Category o′ ℓ′ e′} (L : Functor C D) (R : Functor D C) (J : Functor E C) → L ⊣ R → RelativeAdjoint D J | ⊣⇒RAdjoint {C = C} {D} L R J A = record
{ L = L ∘F J
; R = R
; Hom-NI = record
{ F⇒G = ntHelper record
{ η = λ _ → record { to = Radjunct ; cong = ∘-resp-≈ʳ ∙ L.F-resp-≈ }
; commute = λ _ → Radjunct-comm C.Equiv.refl
}
; F⇐G = ntHelper record
{ η = λ _ → record { to = Ladjunct ; co... | function | definition | ⊣⇒RAdjoint | Categories.Adjoint | src/Categories/Adjoint/Relative.agda | [
"Level",
"Data.Product",
"Function",
"Function.Bundles",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Product",
"Categories.Category.Instance.Setoids",
"Categories.Functor",
"Categories.Functor.Bifunctor",
"Categories.Functor.Hom",
"Categories.Nat... | [
"Adjoint",
"Category",
"Functor",
"L",
"RelativeAdjoint",
"X",
"_",
"ntHelper",
"η"
] | null | 115 | 115 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record _⊣⊢_ (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
field
unit : idF ≃ (R ∘F L)
counit : (L ∘F R) ≃ idF
module unit = NaturalIsomorphism unit
module counit = NaturalIsomorphism counit
private
module C = Category C using (Obj; id; _∘_; _≈_; module HomReas... | record _⊣⊢_ (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
field
unit : idF ≃ (R ∘F L)
counit : (L ∘F R) ≃ idF
module unit = NaturalIsomorphism unit
module counit = NaturalIsomorphism counit
private
module C = Category C using (Obj; id; _∘_; _≈_; module HomReas... | record | structure | _⊣⊢_ | Categories.Adjoint | src/Categories/Adjoint/TwoSided.agda | [
"Level",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.NaturalIsomorphism.Properties",
"Categories.Morphism.Reasonin... | [
"Adjoint",
"B",
"Category",
"Functor",
"L",
"NaturalIsomorphism",
"_∘_",
"_≈_",
"id",
"identity",
"op"
] | null | 28 | 97 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
private
record WithZig (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
field
unit : idF ≃ (R ∘F L)
counit : (L ∘F R) ≃ idF
private
module unit = NaturalIsomorphism unit
module counit = NaturalIsomorphism counit
module C = Category C using (Ob... | private
record WithZig (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ levelOfTerm R) where
field
unit : idF ≃ (R ∘F L)
counit : (L ∘F R) ≃ idF
private
module unit = NaturalIsomorphism unit
module counit = NaturalIsomorphism counit
module C = Category C using (Ob... | record | structure | WithZig | Categories.Adjoint | src/Categories/Adjoint/TwoSided.agda | [
"Level",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.NaturalIsomorphism.Properties",
"Categories.Morphism.Reasonin... | [
"B",
"Category",
"Functor",
"L",
"NaturalIsomorphism",
"_∘_",
"_≈_",
"id",
"identity",
"op"
] | null | 99 | 153 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
id⊣⊢id : idF {C = C} ⊣⊢ idF
id⊣⊢id {C = C} = record
{ unit = ≃.sym ≃.unitor²
; counit = ≃.unitor²
; zig = identity²
; zag = identity²
}
where open Category C | id⊣⊢id : idF {C = C} ⊣⊢ idF | id⊣⊢id {C = C} = record
{ unit = ≃.sym ≃.unitor²
; counit = ≃.unitor²
; zig = identity²
; zag = identity²
}
where open Category C | function | definition | id⊣⊢id | Categories.Adjoint | src/Categories/Adjoint/TwoSided.agda | [
"Level",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.NaturalIsomorphism.Properties",
"Categories.Morphism.Reasonin... | [
"Category"
] | null | 175 | 175 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
record SolutionSet i : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ (suc i)) where
field
I : Set i
S : I → C.Obj
S₀ : ∀ {A X} → X ⇒ F₀ A → I
S₁ : ∀ {A X} (f : X ⇒ F₀ A) → S (S₀ f) C.⇒ A
ϕ : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S (S₀ f))
commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f... | record SolutionSet i : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′ ⊔ (suc i)) where
field
I : Set i
S : I → C.Obj
S₀ : ∀ {A X} → X ⇒ F₀ A → I
S₁ : ∀ {A X} (f : X ⇒ F₀ A) → S (S₀ f) C.⇒ A
ϕ : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S (S₀ f))
commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f... | record | structure | SolutionSet | Categories.Adjoint.AFT | src/Categories/Adjoint/AFT/SolutionSet.agda | [
"Categories.Category",
"Categories.Functor",
"Level"
] | [
"X",
"f"
] | null | 18 | 25 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
record SolutionSet′ : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′) where
field
S₀ : ∀ {A X} → X ⇒ F₀ A → C.Obj
S₁ : ∀ {A X} (f : X ⇒ F₀ A) → S₀ f C.⇒ A
ϕ : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S₀ f)
commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f ≈ f | record SolutionSet′ : Set (o ⊔ ℓ ⊔ o′ ⊔ ℓ′ ⊔ e′) where
field
S₀ : ∀ {A X} → X ⇒ F₀ A → C.Obj
S₁ : ∀ {A X} (f : X ⇒ F₀ A) → S₀ f C.⇒ A
ϕ : ∀ {A X} (f : X ⇒ F₀ A) → X ⇒ F₀ (S₀ f)
commute : ∀ {A X} (f : X ⇒ F₀ A) → F₁ (S₁ f) ∘ ϕ f ≈ f | record | structure | SolutionSet′ | Categories.Adjoint.AFT | src/Categories/Adjoint/AFT/SolutionSet.agda | [
"Categories.Category",
"Categories.Functor",
"Level"
] | [
"X",
"f"
] | null | 28 | 33 | false | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof | |
SolutionSet⇒SolutionSet′ : ∀ {i} → SolutionSet i → SolutionSet′
SolutionSet⇒SolutionSet′ s = record
{ S₀ = λ f → S (S₀ f)
; S₁ = S₁
; ϕ = ϕ
; commute = commute
}
where open SolutionSet s | SolutionSet⇒SolutionSet′ : ∀ {i} → SolutionSet i → SolutionSet′ | SolutionSet⇒SolutionSet′ s = record
{ S₀ = λ f → S (S₀ f)
; S₁ = S₁
; ϕ = ϕ
; commute = commute
}
where open SolutionSet s | function | definition | SolutionSet⇒SolutionSet′ | Categories.Adjoint.AFT | src/Categories/Adjoint/AFT/SolutionSet.agda | [
"Categories.Category",
"Categories.Functor",
"Level"
] | [
"SolutionSet",
"SolutionSet′",
"f"
] | null | 35 | 35 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
SolutionSet′⇒SolutionSet : ∀ i → SolutionSet′ → SolutionSet (o ⊔ i)
SolutionSet′⇒SolutionSet i s = record
{ I = Lift i C.Obj
; S = lower
; S₀ = λ f → lift (S₀ f)
; S₁ = S₁
; ϕ = ϕ
; commute = commute
}
where open SolutionSet′ s | SolutionSet′⇒SolutionSet : ∀ i → SolutionSet′ → SolutionSet (o ⊔ i) | SolutionSet′⇒SolutionSet i s = record
{ I = Lift i C.Obj
; S = lower
; S₀ = λ f → lift (S₀ f)
; S₁ = S₁
; ϕ = ϕ
; commute = commute
}
where open SolutionSet′ s | function | definition | SolutionSet′⇒SolutionSet | Categories.Adjoint.AFT | src/Categories/Adjoint/AFT/SolutionSet.agda | [
"Categories.Category",
"Categories.Functor",
"Level"
] | [
"SolutionSet",
"SolutionSet′",
"f"
] | null | 44 | 44 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful : Functor CoEilenbergMoore C
Forgetful = record
{ F₀ = Comodule.A
; F₁ = Comodule⇒.arr
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ eq → eq
} | Forgetful : Functor CoEilenbergMoore C | Forgetful = record
{ F₀ = Comodule.A
; F₁ = Comodule⇒.arr
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ eq → eq
} | function | definition | Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoEilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoEilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTrans... | [
"CoEilenbergMoore",
"Functor",
"identity",
"refl"
] | null | 26 | 26 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Cofree : Functor C CoEilenbergMoore
Cofree = record
{ F₀ = λ A → record
{ A = F₀ A
; coaction = M.δ.η A
; commute = M.sym-assoc
; identity = Comonad.identityʳ M
}
; F₁ = λ f → record
{ arr = F₁ f
; commute = M.δ.commute f
}
; identity = identity
; homomorphism = homomorphism
; F-resp-≈ = F-resp-≈
... | Cofree : Functor C CoEilenbergMoore | Cofree = record
{ F₀ = λ A → record
{ A = F₀ A
; coaction = M.δ.η A
; commute = M.sym-assoc
; identity = Comonad.identityʳ M
}
; F₁ = λ f → record
{ arr = F₁ f
; commute = M.δ.commute f
}
; identity = identity
; homomorphism = homomorphism
; F-resp-≈ = F-resp-≈
} | function | definition | Cofree | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoEilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoEilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTrans... | [
"CoEilenbergMoore",
"Functor",
"f",
"identity"
] | null | 35 | 35 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
UC≃M : Forgetful ∘F Cofree ≃ M.F
UC≃M = niHelper (record
{ η = λ _ → F₁ C.id
; η⁻¹ = λ _ → F₁ C.id
; commute = λ f → [ M.F ]-resp-square id-comm-sym
; iso = λ _ → record
{ isoˡ = elimˡ identity ○ identity
; isoʳ = elimˡ identity ○ identity
}
}) | UC≃M : Forgetful ∘F Cofree ≃ M.F | UC≃M = niHelper (record
{ η = λ _ → F₁ C.id
; η⁻¹ = λ _ → F₁ C.id
; commute = λ f → [ M.F ]-resp-square id-comm-sym
; iso = λ _ → record
{ isoˡ = elimˡ identity ○ identity
; isoʳ = elimˡ identity ○ identity
}
}) | function | definition | UC≃M | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoEilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoEilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTrans... | [
"Cofree",
"Forgetful",
"_",
"f",
"identity",
"niHelper",
"η"
] | null | 52 | 52 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful⊣Cofree : Forgetful ⊣ Cofree
Forgetful⊣Cofree = record
{ unit = record
{ η = λ X → let module X = Comodule X
in record
{ arr = X.coaction
; commute = ⟺ X.commute
}
; commute = Comodule⇒.commute
; sym-commute = λ f → ⟺ (Comodule⇒.commute f)
}
; counit = record
{ η =... | Forgetful⊣Cofree : Forgetful ⊣ Cofree | Forgetful⊣Cofree = record
{ unit = record
{ η = λ X → let module X = Comodule X
in record
{ arr = X.coaction
; commute = ⟺ X.commute
}
; commute = Comodule⇒.commute
; sym-commute = λ f → ⟺ (Comodule⇒.commute f)
}
; counit = record
{ η = M.ε.η
; commute = M.ε.commute
; s... | function | definition | Forgetful⊣Cofree | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoEilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoEilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTrans... | [
"B",
"Cofree",
"Comodule",
"Forgetful",
"X",
"f",
"η"
] | null | 63 | 63 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful : Functor (CoKleisli M) C
Forgetful =
record
{ F₀ = λ X → F₀ X
; F₁ = λ f → F₁ f ∘ M.δ.η _
; identity = Comonad.identityˡ M
; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
; F-resp-≈ = λ eq → ∘-resp-≈ˡ (F-resp-≈ eq)
}
where
trihom : {X Y Z W : Obj}... | Forgetful : Functor (CoKleisli M) C | Forgetful =
record
{ F₀ = λ X → F₀ X
; F₁ = λ f → F₁ f ∘ M.δ.η _
; identity = Comonad.identityˡ M
; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
; F-resp-≈ = λ eq → ∘-resp-≈ˡ (F-resp-≈ eq)
}
where
trihom : {X Y Z W : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} {h : Z ⇒ W}... | function | definition | Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoKleisli.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoKleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoning"... | [
"CoKleisli",
"Functor",
"X",
"_",
"f",
"g",
"identity",
"sym"
] | null | 25 | 25 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Cofree : Functor C (CoKleisli M)
Cofree =
record
{ F₀ = λ X → X
; F₁ = λ f → f ∘ M.ε.η _
; identity = λ {A} → identityˡ
; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
; F-resp-≈ = λ x → ∘-resp-≈ˡ x
}
where
hom-proof :
{X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} →
(g ∘ f) ∘ M.ε.η X ≈ (... | Cofree : Functor C (CoKleisli M) | Cofree =
record
{ F₀ = λ X → X
; F₁ = λ f → f ∘ M.ε.η _
; identity = λ {A} → identityˡ
; homomorphism = λ {X Y Z} {f g} → hom-proof {X} {Y} {Z} {f} {g}
; F-resp-≈ = λ x → ∘-resp-≈ˡ x
}
where
hom-proof :
{X Y Z : Obj} {f : X ⇒ Y} {g : Y ⇒ Z} →
(g ∘ f) ∘ M.ε.η X ≈ (g ∘ M.ε.η Y) ∘ (F₁ (f ∘ M.ε.η X) ... | function | definition | Cofree | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoKleisli.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoKleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoning"... | [
"CoKleisli",
"Functor",
"X",
"_",
"f",
"g",
"identity",
"sym",
"x"
] | null | 50 | 50 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
FC≃M : Forgetful ∘F Cofree ≃ M.F
FC≃M =
record
{ F⇒G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → to-commute {X} {Y} f
}
; F⇐G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → from-commute {X} {Y} f
}
; iso = λ X → record
{ isoˡ = elimʳ identity ○ identit... | FC≃M : Forgetful ∘F Cofree ≃ M.F | FC≃M =
record
{ F⇒G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → to-commute {X} {Y} f
}
; F⇐G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → from-commute {X} {Y} f
}
; iso = λ X → record
{ isoˡ = elimʳ identity ○ identity
; isoʳ = elimʳ identity ○ i... | function | definition | FC≃M | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoKleisli.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoKleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoning"... | [
"Cofree",
"Forgetful",
"X",
"f",
"identity",
"ntHelper",
"sym",
"η"
] | null | 69 | 69 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
FF1≈1 : {X : Obj} → F₁ (F₁ (C.id {X})) ≈ C.id
FF1≈1 {X} = begin
F₁ (F₁ (C.id {X})) ≈⟨ F-resp-≈ identity ⟩
F₁ (C.id) ≈⟨ identity ⟩
C.id ∎ | FF1≈1 : {X : Obj} → F₁ (F₁ (C.id {X})) ≈ C.id | FF1≈1 {X} = begin
F₁ (F₁ (C.id {X})) ≈⟨ F-resp-≈ identity ⟩
F₁ (C.id) ≈⟨ identity ⟩
C.id ∎ | function | definition | FF1≈1 | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoKleisli.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoKleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoning"... | [
"X",
"identity"
] | null | 101 | 101 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful⊣Cofree : Forgetful ⊣ Cofree
Forgetful⊣Cofree =
record
{ unit = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → unit-commute {X} {Y} f
}
; counit = ntHelper record
{ η = M.ε.η
; commute = λ {X Y} f → counit-commute {X} {Y} f
}
; zig = λ {A} → zig-proof {A}
; zag = λ... | Forgetful⊣Cofree : Forgetful ⊣ Cofree | Forgetful⊣Cofree =
record
{ unit = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → unit-commute {X} {Y} f
}
; counit = ntHelper record
{ η = M.ε.η
; commute = λ {X Y} f → counit-commute {X} {Y} f
}
; zig = λ {A} → zig-proof {A}
; zag = λ {B} → zag-proof {B}
}
where
uni... | function | definition | Forgetful⊣Cofree | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/CoKleisli.agda | [
"Categories.Category.Core",
"Categories.Comonad",
"Categories.Category.Construction.CoKleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoning"... | [
"B",
"Cofree",
"FF1≈1",
"Forgetful",
"X",
"_",
"f",
"identity",
"ntHelper",
"sym",
"η"
] | null | 107 | 107 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful : Functor EilenbergMoore C
Forgetful = record
{ F₀ = Module.A
; F₁ = Module⇒.arr
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ eq → eq
} | Forgetful : Functor EilenbergMoore C | Forgetful = record
{ F₀ = Module.A
; F₁ = Module⇒.arr
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ eq → eq
} | function | definition | Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/EilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.EilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoni... | [
"EilenbergMoore",
"Functor",
"identity",
"refl"
] | null | 24 | 24 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Free : Functor C EilenbergMoore
Free = record
{ F₀ = λ A → record
{ A = F₀ A
; action = M.μ.η A
; commute = M.assoc
; identity = M.identityʳ
}
; F₁ = λ f → record
{ arr = F₁ f
; commute = ⟺ (M.μ.commute f)
}
; identity = identity
; homomorphi... | Free : Functor C EilenbergMoore | Free = record
{ F₀ = λ A → record
{ A = F₀ A
; action = M.μ.η A
; commute = M.assoc
; identity = M.identityʳ
}
; F₁ = λ f → record
{ arr = F₁ f
; commute = ⟺ (M.μ.commute f)
}
; identity = identity
; homomorphism = homomorphism
; F-resp-≈ ... | function | definition | Free | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/EilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.EilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoni... | [
"EilenbergMoore",
"Functor",
"f",
"identity"
] | null | 33 | 33 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
FF≃F : Forgetful ∘F Free ≃ M.F
FF≃F = record
{ F⇒G = record
{ η = λ _ → F₁ C.id
; commute = λ _ → [ M.F ]-resp-square id-comm-sym
; sym-commute = λ _ → [ M.F ]-resp-square id-comm
}
; F⇐G = record
{ η = λ _ → F₁ C.id
; commute = λ _ → [ M.F ]-resp-square id-comm-sym
;... | FF≃F : Forgetful ∘F Free ≃ M.F | FF≃F = record
{ F⇒G = record
{ η = λ _ → F₁ C.id
; commute = λ _ → [ M.F ]-resp-square id-comm-sym
; sym-commute = λ _ → [ M.F ]-resp-square id-comm
}
; F⇐G = record
{ η = λ _ → F₁ C.id
; commute = λ _ → [ M.F ]-resp-square id-comm-sym
; sym-commute = λ _ → [ M.F ]-re... | function | definition | FF≃F | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/EilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.EilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoni... | [
"Forgetful",
"Free",
"_",
"identity",
"η"
] | null | 50 | 50 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Free⊣Forgetful : Free ⊣ Forgetful
Free⊣Forgetful = record
{ unit = record
{ η = M.η.η
; commute = M.η.commute
; sym-commute = M.η.sym-commute
}
; counit = record
{ η = λ X →
let module X = Module X
in record
{ arr = X.action
; commute = ⟺... | Free⊣Forgetful : Free ⊣ Forgetful | Free⊣Forgetful = record
{ unit = record
{ η = M.η.η
; commute = M.η.commute
; sym-commute = M.η.sym-commute
}
; counit = record
{ η = λ X →
let module X = Module X
in record
{ arr = X.action
; commute = ⟺ X.commute
}
; commute... | function | definition | Free⊣Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/EilenbergMoore.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.EilenbergMoore",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categories.Morphism.Reasoni... | [
"B",
"Forgetful",
"Free",
"Module",
"X",
"f",
"η"
] | null | 68 | 68 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Forgetful : Functor (Kleisli M) C
Forgetful = record
{ F₀ = λ X → F₀ X
; F₁ = λ f → μ.η _ ∘ F₁ f
; identity = M.identityˡ
; homomorphism = λ {X Y Z} {f g} → begin
μ.η Z ∘ F₁ ((μ.η Z ∘ F₁ g) ∘ f) ≈⟨ refl⟩∘⟨ homomorphism ⟩
μ.η Z ∘ F₁ (μ.η Z ∘ F₁ g) ∘ F₁ f ≈⟨ refl⟩∘⟨ ... | Forgetful : Functor (Kleisli M) C | Forgetful = record
{ F₀ = λ X → F₀ X
; F₁ = λ f → μ.η _ ∘ F₁ f
; identity = M.identityˡ
; homomorphism = λ {X Y Z} {f g} → begin
μ.η Z ∘ F₁ ((μ.η Z ∘ F₁ g) ∘ f) ≈⟨ refl⟩∘⟨ homomorphism ⟩
μ.η Z ∘ F₁ (μ.η Z ∘ F₁ g) ∘ F₁ f ≈⟨ refl⟩∘⟨ homomorphism ⟩∘⟨refl ⟩
μ.η Z ∘... | function | definition | Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/Kleisli.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.Kleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Morphism",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categorie... | [
"Functor",
"Kleisli",
"X",
"_",
"center",
"f",
"g",
"identity",
"pull-first",
"refl"
] | null | 26 | 26 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Free : Functor C (Kleisli M)
Free = record
{ F₀ = λ X → X
; F₁ = λ f → η.η _ ∘ f
; identity = C.identityʳ
; homomorphism = λ {X Y Z} {f g} → begin
η.η Z ∘ g ∘ f ≈⟨ sym-assoc ○ ⟺ identityˡ ⟩
C.id ∘ (η.η Z ∘ g) ∘ f ≈˘⟨ pull-first M.ide... | Free : Functor C (Kleisli M) | Free = record
{ F₀ = λ X → X
; F₁ = λ f → η.η _ ∘ f
; identity = C.identityʳ
; homomorphism = λ {X Y Z} {f g} → begin
η.η Z ∘ g ∘ f ≈⟨ sym-assoc ○ ⟺ identityˡ ⟩
C.id ∘ (η.η Z ∘ g) ∘ f ≈˘⟨ pull-first M.identityˡ ⟩
μ.η Z ∘ (F₁ (η.η... | function | definition | Free | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/Kleisli.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.Kleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Morphism",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categorie... | [
"Functor",
"Kleisli",
"X",
"_",
"center",
"f",
"g",
"identity",
"pull-first"
] | null | 41 | 41 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
FF≃F : Forgetful ∘F Free ≃ M.F
FF≃F = record
{ F⇒G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → begin
F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y ∘ f) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ homomorphism ⟩
F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f ≈⟨ refl⟩∘⟨ cancelˡ M.identityˡ ⟩
F₁ C.id ∘ F₁ f ... | FF≃F : Forgetful ∘F Free ≃ M.F | FF≃F = record
{ F⇒G = ntHelper record
{ η = λ X → F₁ C.id
; commute = λ {X Y} f → begin
F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y ∘ f) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ homomorphism ⟩
F₁ C.id ∘ μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f ≈⟨ refl⟩∘⟨ cancelˡ M.identityˡ ⟩
F₁ C.id ∘ F₁ f ≈⟨ [ M.F ]-resp-s... | function | definition | FF≃F | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/Kleisli.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.Kleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Morphism",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categorie... | [
"Forgetful",
"Free",
"X",
"f",
"identity",
"ntHelper",
"η"
] | null | 55 | 55 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Free⊣Forgetful : Free ⊣ Forgetful
Free⊣Forgetful = record
{ unit = ntHelper record
{ η = η.η
; commute = λ {X Y} f → begin
η.η Y ∘ f ≈⟨ η.commute f ⟩
F₁ f ∘ η.η X ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
(μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f) ∘ η.η X ... | Free⊣Forgetful : Free ⊣ Forgetful | Free⊣Forgetful = record
{ unit = ntHelper record
{ η = η.η
; commute = λ {X Y} f → begin
η.η Y ∘ f ≈⟨ η.commute f ⟩
F₁ f ∘ η.η X ≈˘⟨ cancelˡ M.identityˡ ⟩∘⟨refl ⟩
(μ.η Y ∘ F₁ (η.η Y) ∘ F₁ f) ∘ η.η X ≈˘⟨ ∘-resp-≈ʳ homomorphism ⟩∘⟨ref... | function | definition | Free⊣Forgetful | Categories.Adjoint.Construction | src/Categories/Adjoint/Construction/Kleisli.agda | [
"Categories.Category.Core",
"Categories.Monad",
"Categories.Category.Construction.Kleisli",
"Categories.Adjoint",
"Categories.Functor",
"Categories.Morphism",
"Categories.Functor.Properties",
"Categories.NaturalTransformation.Core",
"Categories.NaturalTransformation.NaturalIsomorphism",
"Categorie... | [
"B",
"Forgetful",
"Free",
"X",
"f",
"identity",
"ntHelper",
"η"
] | null | 79 | 79 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e)
Inclusion {c} {ℓ} e = record
{ F₀ = 0-Groupoid e
; F₁ = λ f → record { F₀ = to f; F₁ = cong f }
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ {S T f g} f≗g →
let module S = Setoid S
module T = Seto... | Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e) | Inclusion {c} {ℓ} e = record
{ F₀ = 0-Groupoid e
; F₁ = λ f → record { F₀ = to f; F₁ = cong f }
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ {S T f g} f≗g →
let module S = Setoid S
module T = Setoid T
in record
{ F⇒G = record { η = λ _ → f≗g }
... | function | definition | Inclusion | Categories.Adjoint.Instance | src/Categories/Adjoint/Instance/0-Truncation.agda | [
"Function.Base",
"Function.Bundles",
"Function.Construct.Identity",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Construction.0-Groupoid",
"Categories.Category.Groupoid",
"Categories.Category.Instance.Groupoids",
"Categories.Category.Instance.Setoids",
... | [
"0-Groupoid",
"Functor",
"Groupoids",
"Setoids",
"Trunc",
"_",
"f",
"g",
"identity",
"refl",
"η"
] | null | 26 | 26 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
TruncAdj {o} {ℓ} {e} = record
{ unit = unit
; counit = counit
; zig = λ {A} → Category.id (category A)
; zag = refl
}
where
open Func
open Groupoid using (category)
unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
unit = reco... | TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e | TruncAdj {o} {ℓ} {e} = record
{ unit = unit
; counit = counit
; zig = λ {A} → Category.id (category A)
; zag = refl
}
where
open Func
open Groupoid using (category)
unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
unit = record
{ η = λ _ → record { F₀ = id→ ; ... | function | definition | TruncAdj | Categories.Adjoint.Instance | src/Categories/Adjoint/Instance/0-Truncation.agda | [
"Function.Base",
"Function.Bundles",
"Function.Construct.Identity",
"Relation.Binary",
"Categories.Adjoint",
"Categories.Category.Core",
"Categories.Category.Construction.0-Groupoid",
"Categories.Category.Groupoid",
"Categories.Category.Instance.Groupoids",
"Categories.Category.Instance.Setoids",
... | [
"Groupoid",
"Inclusion",
"NaturalTransformation",
"Trunc",
"_",
"ntHelper",
"refl",
"η"
] | null | 44 | 44 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
Inclusion : ∀ {c ℓ₁ ℓ₂} e → Functor (Posets c ℓ₁ ℓ₂) (Cats c ℓ₂ e)
Inclusion {c} {ℓ₁} e = record
{ F₀ = Thin e
; F₁ = λ f → record { F₀ = ⟦ f ⟧ ; F₁ = mono f }
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ {A B f g} f≗g →
let open Poset B
in record
{ F⇒G = reco... | Inclusion : ∀ {c ℓ₁ ℓ₂} e → Functor (Posets c ℓ₁ ℓ₂) (Cats c ℓ₂ e) | Inclusion {c} {ℓ₁} e = record
{ F₀ = Thin e
; F₁ = λ f → record { F₀ = ⟦ f ⟧ ; F₁ = mono f }
; identity = refl
; homomorphism = refl
; F-resp-≈ = λ {A B f g} f≗g →
let open Poset B
in record
{ F⇒G = record { η = λ _ → reflexive f≗g }
; F⇐G = record { η = λ ... | function | definition | Inclusion | Categories.Adjoint.Instance | src/Categories/Adjoint/Instance/01-Truncation.agda | [
"Data.Product",
"Function",
"Relation.Binary",
"Relation.Binary.Morphism.Bundles",
"Categories.Adjoint",
"Categories.Category.Construction.Thin",
"Categories.Category",
"Categories.Category.Instance.Cats",
"Categories.Category.Instance.Posets",
"Categories.Functor",
"Categories.Functor.Instance.... | [
"B",
"Cats",
"Functor",
"Poset",
"Posets",
"Thin",
"Trunc",
"_",
"f",
"g",
"identity",
"mono",
"refl",
"η",
"⟦"
] | null | 28 | 28 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
TruncAdj {o} {ℓ} {e} = record
{ unit = unit
; counit = counit
; zig = λ {C} → id C , id C
; zag = refl
}
where
open Category
unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
unit = record
{ η = λ _ → record { F₀ =... | TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e | TruncAdj {o} {ℓ} {e} = record
{ unit = unit
; counit = counit
; zig = λ {C} → id C , id C
; zag = refl
}
where
open Category
unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
unit = record
{ η = λ _ → record { F₀ = Function.id ; F₁ = Function.id }
; commute ... | function | definition | TruncAdj | Categories.Adjoint.Instance | src/Categories/Adjoint/Instance/01-Truncation.agda | [
"Data.Product",
"Function",
"Relation.Binary",
"Relation.Binary.Morphism.Bundles",
"Categories.Adjoint",
"Categories.Category.Construction.Thin",
"Categories.Category",
"Categories.Category.Instance.Cats",
"Categories.Category.Instance.Posets",
"Categories.Functor",
"Categories.Functor.Instance.... | [
"Category",
"Inclusion",
"NaturalTransformation",
"Trunc",
"X",
"_",
"id",
"ntHelper",
"refl",
"η"
] | null | 44 | 44 | true | https://github.com/agda/agda-categories | fbd1259c2dcf011ee1936fa8c24a1b10e6285673 | statement+proof |
End of preview. Expand in Data Studio
Agda-Categories
Structured dataset from agda-categories — Category theory.
Source
- Repository: https://github.com/agda/agda-categories
- Commit:
fbd1259c2dcf011ee1936fa8c24a1b10e6285673 - Files: 521
- License: mit
Schema
| Column | Type | Description |
|---|---|---|
| fact | string | Verbatim declaration: statement followed by proof where present |
| statement | string | Verbatim statement (keyword through the closing period) |
| proof | string | Verbatim proof block (Proof. ... Qed./Defined.), empty if none |
| type | string | Raw declaration keyword |
| kind | string | Normalized kind |
| symbolic_name | string | Declaration identifier |
| library | string | Sub-library |
| filename | string | Repository-relative source path |
| imports | list[string] | File-level Require/Import modules |
| deps | list[string] | Intra-corpus identifiers referenced |
| docstring | string | Preceding documentation comment, null if absent |
| line_start | int | First source line |
| line_end | int | Last source line |
| has_proof | bool | Whether a proof block was captured |
| source_url | string | Upstream repository |
| commit | string | Upstream commit extracted |
| content_level | string | statement+proof |
Statistics
- Entries: 1,269
- With proof: 925 (72.9%)
- With docstring: 0 (0.0%)
- Libraries: 116
By type
| Type | Count |
|---|---|
| function | 1,025 |
| record | 238 |
| data | 6 |
Example
2-Category : (o ℓ e t : Level) → Set (suc (o ⊔ ℓ ⊔ e ⊔ t))
2-Category o ℓ e t = Category (Product.Cats-Monoidal {o} {ℓ} {e}) t
- kind: definition | symbolic_name:
2-Category| src/Categories/2-Category.agda:10
Use
Statement and proof are available both joined (fact) and split (statement, proof) for
proof-term modeling, autoformalization, retrieval, and dependency analysis via deps.
Citation
@misc{agda_categories_dataset,
title = {Agda-Categories},
author = {Norton, Charles},
year = {2026},
note = {Extracted from https://github.com/agda/agda-categories, commit fbd1259c2dcf},
url = {https://huggingface.co/datasets/phanerozoic/Agda-Categories}
}
- Downloads last month
- 35