Last active
June 29, 2021 16:17
-
-
Save daig/f31e6a36c4c8ca2e1921679c04157e4f to your computer and use it in GitHub Desktop.
Chu embeds in Lens
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --type-in-type #-} | |
| module functors where | |
| open import prelude | |
| record Category {O : Set} (𝒞[_,_] : O → O → Set) : Set where | |
| constructor 𝒾:_▸:_𝒾▸:_▸𝒾: | |
| infixl 8 _▸_ | |
| field | |
| 𝒾 : ∀ {x} → 𝒞[ x , x ] | |
| _▸_ : ∀ {x y z} → 𝒞[ x , y ] → 𝒞[ y , z ] → 𝒞[ x , z ] | |
| 𝒾▸ : ∀ {x y} (f : 𝒞[ x , y ]) → (𝒾 ▸ f) ≡ f | |
| ▸𝒾 : ∀ {x y} (f : 𝒞[ x , y ]) → (f ▸ 𝒾) ≡ f | |
| open Category ⦃...⦄ public | |
| record Functor {A : Set} {𝒜[_,_] : A → A → Set} | |
| {B : Set} {ℬ[_,_] : B → B → Set} | |
| (f : A → B) : Set where | |
| constructor φ:_𝒾:_▸: | |
| field | |
| ⦃ cat₁ ⦄ : Category {A} 𝒜[_,_] | |
| ⦃ cat₂ ⦄ : Category {B} ℬ[_,_] | |
| φ : ∀ {a b} → 𝒜[ a , b ] → ℬ[ f a , f b ] | |
| functor-id : ∀ {a} → φ {a} 𝒾 ≡ 𝒾 | |
| functor-comp : ∀ {A B C} → (f : 𝒜[ A , B ]) (g : 𝒜[ B , C ]) | |
| → φ (f ▸ g) ≡ φ f ▸ φ g | |
| open Functor ⦃...⦄ public |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --type-in-type #-} | |
| module chu-lens where | |
| open import prelude | |
| open import functors | |
| open import chu | |
| open import lens | |
| →∫ : Chu → ∫ | |
| →∫ (A⁺ , A⁻ ! Ω) = A⁺ , λ a⁺ → ∃ (Ω a⁺) | |
| →Lens : {A B : Chu} → Chu[ A , B ] → ∫[ →∫ A , →∫ B ] | |
| →Lens (f ↔ fᵗ ! †) a⁺ = f a⁺ , λ (b⁻ , fa⁺Ωb⁻) → fᵗ b⁻ , subst id († a⁺ b⁻) fa⁺Ωb⁻ | |
| module _ {A B C : Chu} | |
| (F@(f ↔ fᵗ ! _†₁_) : Chu[ A , B ]) | |
| (G@(g ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where | |
| comp₂ : ∀ a⁺ → π₂ (→Lens (F ▸ G) a⁺) | |
| ≡ π₂ ((→Lens F ▸ →Lens G) a⁺) | |
| comp₂ a⁺ = extensionality λ ( c⁻ , gfaΩc ) → (λ x → (fᵗ ∘ gᵗ) c⁻ , x) ⟨$⟩ | |
| subst⋯ id (f a⁺ †₂ c⁻) (a⁺ †₁ gᵗ c⁻) gfaΩc | |
| comp∀ : ∀ a⁺ → →Lens (F ▸ G) a⁺ ≡ (→Lens F ▸ →Lens G) a⁺ | |
| comp∀ a⁺ rewrite comp₂ a⁺ = refl | |
| instance | |
| open Chu[_,_] | |
| chu-lens-functor : Functor →∫ | |
| chu-lens-functor = φ: →Lens | |
| 𝒾: refl | |
| ▸: λ F G → extensionality (comp∀ F G) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --type-in-type #-} | |
| module chu where | |
| open import functors | |
| open import prelude | |
| record Chu : Set where | |
| constructor _,_!_ | |
| field | |
| _⁺ _⁻ : Set | |
| _Ω_ : _⁺ → _⁻ → Set | |
| module _ (A@(A⁺ , A⁻ ! _Ω₁_) B@(B⁺ , B⁻ ! _Ω₂_) : Chu) where | |
| record Chu[_,_] : Set where -- Morphisms of chu spaces | |
| constructor _↔_!_ | |
| field | |
| to : A⁺ → B⁺ | |
| from : B⁻ → A⁻ | |
| adj : ∀ a⁺ b⁻ → to a⁺ Ω₂ b⁻ ≡ a⁺ Ω₁ from b⁻ | |
| module _ {A@(A⁺ , A⁻ ! _Ω₁_) | |
| B@(B⁺ , B⁻ ! _Ω₂_) | |
| C@(C⁺ , C⁻ ! _Ω₃_) : Chu} | |
| (F@(f ↔ fᵗ ! _†₁_) : Chu[ A , B ]) | |
| (G@(g ↔ gᵗ ! _†₂_) : Chu[ B , C ]) where | |
| adj-comp : ∀ a⁺ c⁻ → (g ∘ f) a⁺ Ω₃ c⁻ ≡ a⁺ Ω₁ (fᵗ ∘ gᵗ) c⁻ | |
| adj-comp a⁺ c⁻ = trans (f a⁺ †₂ c⁻) -- g (f a⁺) Ω₃ c⁻ | |
| ( a⁺ †₁ gᵗ c⁻) -- f a⁺ Ω₂ gᵗ c⁻ | |
| -- a⁺ Ω₁ fᵗ (gᵗ c⁻) | |
| chu-comp : Chu[ A , C ] | |
| chu-comp = (g ∘ f) ↔ (fᵗ ∘ gᵗ) ! adj-comp | |
| instance | |
| chu-cat : Category Chu[_,_] | |
| chu-cat = 𝒾: (id ↔ id ! λ _ _ → refl) | |
| ▸: chu-comp | |
| 𝒾▸: (λ (_ ↔ _ ! _†_) → (λ x → _ ↔ _ ! x) ⟨$⟩ | |
| extensionality2 λ a⁺ b⁻ → trans-refl (a⁺ † b⁻)) | |
| ▸𝒾: (λ _ → refl) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# OPTIONS --type-in-type #-} | |
| module lens where | |
| open import functors | |
| open import prelude | |
| _^ : Set → Set -- Presheaf | |
| I ^ = I → Set | |
| ∫ : Set -- Arena | |
| ∫ = ∃ _^ | |
| _⦅_⦆ : ∫ → Set → Set -- Interpret as a polynomial functor | |
| (A⁺ , A⁻) ⦅ y ⦆ = Σ[ a⁺ ∈ A⁺ ] (A⁻ a⁺ → y) | |
| module _ (A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫) where | |
| ∫[_,_] : Set | |
| ∫[_,_] = (a⁺ : A⁺) → Σ[ b⁺ ∈ B⁺ ] (B⁻ b⁺ → A⁻ a⁺) | |
| module _ {A@(A⁺ , A⁻) B@(B⁺ , B⁻) : ∫} where | |
| lens : (get : A⁺ → B⁺) | |
| (set : (a⁺ : A⁺) → B⁻ (get a⁺) → A⁻ a⁺) | |
| → ∫[ A , B ] | |
| lens g s = λ a⁺ → g a⁺ , s a⁺ | |
| get : (l : ∫[ A , B ]) → A⁺ → B⁺ | |
| get l = π₁ ∘ l | |
| set : (A↝B : ∫[ A , B ]) → (a⁺ : A⁺) → B⁻ (get A↝B a⁺) → A⁻ a⁺ | |
| set l = π₂ ∘ l | |
| instance | |
| lens-cat : Category ∫[_,_] | |
| lens-cat = 𝒾: (λ a⁺ → a⁺ , id) | |
| ▸: (λ l1 l2 a⁺ → let b⁺ , setb = l1 a⁺ | |
| c⁺ , setc = l2 b⁺ | |
| in c⁺ , setb ∘ setc) | |
| 𝒾▸: (λ _ → refl) | |
| ▸𝒾: (λ _ → refl) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module prelude where | |
| open import Function using (id; _∘_) public | |
| open import Data.Sum renaming (inj₁ to Σ₁; inj₂ to Σ₂) using (_⊎_) public | |
| open import Data.Product renaming (proj₁ to π₁; proj₂ to π₂) using (Σ; _×_; _,_; ∃; Σ-syntax) public | |
| open import Agda.Builtin.Unit using (⊤; tt) public | |
| open import Data.Empty using (⊥) public | |
| open import Data.Nat as Nat renaming (suc to ℕs; zero to ℕz; _+_ to _ℕ+_) using (ℕ) public | |
| open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_; _≢_; refl; sym; trans; subst) renaming (cong to _⟨$⟩_) public | |
| open Eq.≡-Reasoning using (_≡⟨⟩_; step-≡; _∎) public | |
| postulate | |
| extensionality : {A : Set} {B : A → Set} {f g : (x : A) → B x} | |
| → (∀ x → f x ≡ g x) → f ≡ g | |
| extensionality2 : {A : Set} {B : A → Set} {C : (x : A) → B x → Set} {f g : (x : A) (y : B x) → C x y } | |
| → (∀ x y → f x y ≡ g x y) → f ≡ g | |
| extensionality2 λλf≡g = extensionality λ x → extensionality λ y → λλf≡g x y | |
| trans-refl : {A : Set} {x y : A} (p : x ≡ y) → trans p refl ≡ p | |
| trans-refl p rewrite p = refl |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment