blob: fa46290c8ad9de0c91e24f73cd0a6d73eab3a40a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
{-# OPTIONS --without-K --safe #-}
module Functor.Cartesian.Instance.InducedSetoid where
-- The induced setoid functor is cartesian
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-CartesianCategory)
open import Categories.Functor.Cartesian using (CartesianF)
open import Categories.Object.Product using (IsProduct)
open import Category.Cartesian.Instance.Preorders.Primitive using (Preorders-CC)
open import Data.Product using (<_,_>; _,_)
open import Function using (Func)
open import Functor.Free.Instance.InducedSetoid using () renaming (InducedSetoid to IS)
open import Level using (Level)
open import Preorder.Primitive using (Preorder; module Isomorphism)
module _ {c ℓ : Level} where
private
module Preorders-CC = CartesianCategory (Preorders-CC c ℓ)
module BP = BinaryProducts (Preorders-CC.products)
IS-resp-×
: {A B : Preorder c ℓ}
→ IsProduct (Setoids c ℓ) (IS.₁ {B = A} (BP.π₁ {B = B})) (IS.₁ BP.π₂)
IS-resp-× {A} {B} = record
{ ⟨_,_⟩ = λ {S} S⟶ₛIS₀A S⟶ₛIS₀B → let open Func in record
{ to = < to S⟶ₛIS₀A , to S⟶ₛIS₀B >
; cong = λ x≈y → let open Isomorphism._≅_ in record
{ from = from (cong S⟶ₛIS₀A x≈y) , from (cong S⟶ₛIS₀B x≈y)
; to = to (cong S⟶ₛIS₀A x≈y) , to (cong S⟶ₛIS₀B x≈y)
}
}
; project₁ = Isomorphism.≅.refl A
; project₂ = Isomorphism.≅.refl B
; unique = λ {S} {h} {i} {j} π₁∙h≈i π₂∙h≈j {x} → let open Isomorphism._≅_ in record
{ from = to (π₁∙h≈i {x}) , to (π₂∙h≈j {x})
; to = from (π₁∙h≈i {x}) , from (π₂∙h≈j {x})
}
}
InducedSetoid : CartesianF (Preorders-CC c ℓ) (Setoids-CartesianCategory c ℓ)
InducedSetoid = record
{ F = IS
; isCartesian = record
{ F-resp-⊤ = _
; F-resp-× = IS-resp-×
}
}
module InducedSetoid = CartesianF InducedSetoid
|
