Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: [2,C] is cartesian closed, in agda

view this post on Zulip fosco (Oct 17 2021 at 09:19):

I am trying to prove the following fact

the category C2{\cal C}^2 of arrows of a cartesian closed category C\cal C is cartesian closed.

in the particular case of C{\cal C}= the category of sets, using agda, and in particular agda-categories.

Here's a MWE of what I did and where I am stuck (with little effort this entire post is already a lagda file):

First, the minimal possible amount of boilerplate:

module ArrowIsCCC where

open import Categories.Category.CartesianClosed.Canonical
open import Categories.Category.Core
open import Data.Product
open import Function using (const)
open import Level
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality
open Relation.Binary.PropositionalEquality.≡-Reasoning

a postulate on extensionality, because most of the proofs of uniqueness of a terminal object require the lemma for which the terminal type has a unique term ⊤\top, and extensionality to "lift" this to an equality of functions into tt, and the definition of said terminal type tt.

postulate
 extensionality : ∀ {A B : Set} {f g : A → B} →
  (∀ (x : A) → f x ≡ g x) →
  f ≡ g

data t : Set where
 ⊤ : t

!-unique-lemma : ∀ (x : t) → ⊤ ≡ x
!-unique-lemma ⊤ = refl

Now, the arrow category has objects the morphisms of Set and
morphisms the commutative squares

A→B↓↓C→D \begin{array}{ccc} A &\to& B\\ \downarrow && \downarrow \\ C &\to & D\end{array}

arrow : Category (suc zero) zero zero
arrow = record
  { Obj = Σ (Set × Set) (λ x → proj₁ x → proj₂ x)
  ; _⇒_ = arr
  ; _≈_ = _≡_
  ; id = (λ z → z) , λ z → z
  ; _∘_ = λ {A} {B} {C} f g → comp {A} {B} {C} f g
  ; assoc = refl
  ; sym-assoc = refl
  ; identityˡ = refl
  ; identityʳ = refl
  ; identity² = refl
  ; equiv = record { refl = refl ; sym = sym ; trans = trans }
  ; ∘-resp-≈ = λ {refl refl → refl}
  }
  where
  arr : Rel (Σ (Set × Set) (λ x → proj₁ x → proj₂ x)) zero
  arr ((a , b) , x1) ((c , d) , y1) = (a → c) × (b → d)
  comp : {A B C : Σ (Set × Set) (λ x → proj₁ x → proj₂ x)} → arr B C → arr A B → arr A C
  comp {A} {B} {C} (f0 , f1) (g0 , g1) = (λ x → f0 (g0 x)) , λ x → f1 (g1 x)

No particular surprises here (in agda-categories a category Category ℓ o h is indexed over a universe Set o of objects and a universe Set h of morphisms, and lives in a universe Set ℓ); _⇒_ is the relation of morphisms, _≈_ an equivalence relation on each hom-setoid, id and _∘_ identity and composition, et cetera. See the definition of category for how the propositions from assoc to ∘-resp-≈ are defined.

Now, the proof that C2\mathcal{C}^2 is cartesian closed requires another record with a lot of fields:

arrow-ccc : CartesianClosed arrow
arrow-ccc = record
 { ⊤ = (t , t) , (λ _ → ⊤)
 ; _×_ = prod
 ; ! = (λ _ → ⊤) , (λ _ → ⊤)
 ; π₁ = proj₁ , proj₁
 ; π₂ = proj₂ , proj₂
 ; ⟨_,_⟩ = λ {A} {B} {C} f g → pair {A} {B} {C} f g
 ; !-unique = λ {A} → bang-uniq {A}
 ; π₁-comp = refl
 ; π₂-comp = refl
 ; ⟨,⟩-unique = λ {refl refl → refl}
 ; _^_ = to-the
 ; eval = {!   !}
 ; curry = {!   !}
 ; eval-comp = {!   !}
 ; curry-resp-≈ = {!   !}
 ; curry-unique = {!   !}
 }
 where
 prod : Category.Obj arrow → Category.Obj arrow → Category.Obj arrow
 prod ((X , Y) , u) ((A , B) , v) =
  ((X × A) , (Y × B)) , λ x → (u (proj₁ x)) , (v (proj₂ x))
 pair : {C A B : Category.Obj arrow} →
  (arrow Category.⇒ C) A →
  (arrow Category.⇒ C) B →
  (arrow Category.⇒ C) (prod A B)
 pair {(X , Y) , u} {(A , B) , v} {(E , F) , w} (f0 , f1) (g0 , g1) =
  (λ x → (f0 x) , (g0 x)) , (λ x → (f1 x) , (g1 x))
 bang-uniq : {A : Category.Obj arrow} →
  (f : (arrow Category.⇒ A) ((t , t) , (λ _ → ⊤))) →
  ((λ _ → ⊤) , (λ _ → ⊤)) ≡ f
 bang-uniq (f0 , f1) =
  cong₂ _,_
   (extensionality λ x → !-unique-lemma (f0 x))
   (extensionality (λ x → !-unique-lemma (f1 x)))
 to-the : Category.Obj arrow →
  Category.Obj arrow →
  Category.Obj arrow
 to-the ((B0 , B1) , u) ((A0 , A1) , v) =
  (p , (B1 → A1)) , (λ x b1 → {!   !})
   where
   p : Set
   p = Σ ((A0 → B0) × (A1 → B1)) (λ r → (λ x → u ((proj₁ r) x)) ≡ (λ x → (proj₂ r) (v x)))

...and this becomes a bit of a mess. The definition I'm stuck at is the _^_ operation, the internal hom: it is well-known that in an arrow category the internal hom structure is defined by a "pullback-power" construction, defined as a certain pullback. This is what I was trying to do with that 

p : Set
p = Σ ((A0 → B0) × (A1 → B1)) λ r → (λ x → u ((proj₁ r) x)) ≡ (λ x → (proj₂ r) (v x))

the pullback-power [v,u][v,u] should be a dependent sum of all the s,ts,t such that tv=ustv=us (this is exactly how you describe the pullback, indeed).

How can this be defined in agda?

view this post on Zulip Kenji Maillard (Oct 17 2021 at 09:43):

Is it really supposed to be B1 -> A1 in the definition of to-the ? I would have expected something like

to-the ((B0 , B1) , u) ((A0 , A1) , v) =
  (p , (A1 → B1)) , (λ x a1 → proj₂ (proj₁ x) a1)

(I didn't try it though)

view this post on Zulip fosco (Oct 17 2021 at 10:38):

Whoops, yes, that's a mistake. Hmm, and when I write

to-the : Category.Obj arrow →
  Category.Obj arrow →
  Category.Obj arrow
 to-the ((B0 , B1) , u) ((A0 , A1) , v) =
  (p , (A1 → B1)) , (λ x a1 → proj₂ (proj₁ x) a1)
   where
   p : Set
   p = Σ ((A0 → B0) × (A1 → B1)) (λ r → (λ x → u ((proj₁ r) x)) ≡ (λ x → (proj₂ r) (v x)))

nobody complains. Let's see... The next step is defining ev:

ev : {B A : Category.Obj arrow} → (arrow Category.⇒ prod (to-the B A) A) B
ev {(B0 , B1) , u} {(A0 , A1)  , v} = dis , dat
 where
 dis : proj₁ (proj₁ (prod (to-the ((B0 , B1) , u) ((A0 , A1) , v)) ((A0 , A1) , v))) → B0
 dis ((d , p) , a0) = (proj₁ d) a0
 dat : proj₂ (proj₁ (prod (to-the ((B0 , B1) , u) ((A0 , A1) , v)) ((A0 , A1) , v))) → B1
 dat (fst , snd) = fst snd

(probably not the smartest/cleanest way but it works); I am confused though: is p even necessary in the first place?

Something dual happens with curry:

cur : {C A B : Category.Obj arrow} →
 (arrow Category.⇒ (prod C A)) B →
 (arrow Category.⇒ C) (to-the B A)
cur {(C0 , C1) , u} {(A0 , A1) , v} {(B0 , B1) , w} (fst , snd) =
 (λ x → ((λ t → fst (x , t)) , λ t → snd (u x , t)) , extensionality (λ a0 → {!   !})) , (λ z z₁ → snd (z , z₁))

from where should I extract a proof that w (fst (x , a0)) ≡ snd (u x , v a0) (=the type of the hole)?

view this post on Zulip Jacques Carette (Oct 17 2021 at 13:05):

If you put open Category arrow in your where clause, your signatures will be quite a bit simpler.

Your names make it hard to see exactly what's going on, but isn't the type of the hole related to the type of the p in to-the?