How does one write (and debug) a two arguement dependent application, apd2, and use this to prove functoriality of such ap in agda?

1
votes

I'm trying to prove the functoriality of ap under the dependent product type, analgous to Theorem 2.6.5 in the HoTT book, in Agda, and am stuck as to how to how to present the type for he functoriality condition in the presence of the dependent type, as it requires transport. The book suggests this as an exercise at the end of section 2.7.

functorDProdEq : {A A' : Set} {P : A → Set} {Q : A' → Set} (g : A → A')
                 (h : (a : A) →  P a → Q (g a))
                 → ((x1 , y1) (x2 , y2) : Σ A λ a → P a)
                 → (p : x1 ≡ x2) (q : p* {p = p} y1 ≡ y2)
                 → apf (λ - → fDprod g h -) (dpair= (p , q))
                 ≡ dpair= ((apf g p , {!apd (ap2 h ? ?)!} ))
functorDProdEq = {!!}

Above is the attempted definition, with a standalone file below from which the supporting material can be found. The goal in the hole is :

Goal: p* (h (fst .patternInTele0) (snd .patternInTele0)) ≡
      h (fst .patternInTele1) (snd .patternInTele1)

In a context seen below. I don't understand the patternInTele* business, as I don't know where it would have been declared, and would greatly appreciate any elaboration. Additionally, my thought to implement a dependent application function with two equalities, ap2d, the second equality induced by the transportation of the former.

ap2d : {A : Set} {x x' : A}  {P : A → Set} {y : P x} {y' : P x'} {C : (x : A)
  → P x → Set} (f : (x : A) → (y : P x) → C x y )
  → (p : x ≡ x') → (q : (p *) y ≡ y') →
  p* {p = p} f x y ≡ {!!}
  -- p* {p = q} (p* {p = p} (f x)) y ≡ {!f x' y'!}
  -- (f x y ≡ f x' y')
ap2d = {!!}

However, I can't even get this to work. It seems that one would perform a double transport to get the desired result, but nothing I do on the lhs of the final equality seems to change the goal, which is always C x y instead of the desired C x' y'. Is this the proper way to think about defining what I'm after, and does this help solve the original problem of producing a correct functorial theorem statement? What is the correct way to implement both functorDProdEq and ap2d in this context such that they economize on space, as the type signatures tend to get hairy?

--the context from above
y2 : P (fst .patternInTele1)
y2 = snd .patternInTele1
x2 : A
x2 = fst .patternInTele1
y1 : P (fst .patternInTele0)
y1 = snd .patternInTele0
x1 : A
x1 = fst .patternInTele0
q  : p* (snd .patternInTele0) ≡ snd .patternInTele1
p  : fst .patternInTele0 ≡ fst .patternInTele1
.patternInTele1
   : Σ A (λ a → P a)   (not in scope)
.patternInTele0
   : Σ A (λ a → P a)   (not in scope)
h  : (a : A) → P a → Q (g a)
g  : A → A'
Q  : A' → Set
P  : A → Set
A' : Set
A  : Set

And, finally, here's the code.

module question where

open import Agda.Builtin.Sigma public

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}
    → (D : (x y : A) → (x ≡ y) →  Set)
    -- → (d : (a : A) → (D a a r ))
    → ((a : A) → (D a a r ))
    → (x y : A)
    → (p : x ≡ y)
    ------------------------------------
    → D x y p
J D d x .x r = d x

-- ap\_
apf : {A B : Set} → {x y : A} → (f : A → B) → (x ≡ y) → f x ≡ f y
apf {A} {B} {x} {y} f p = J D d x y p
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = {f : A → B} → f x ≡ f y
    d : (x : A) → D x x r
    d = λ x → r 

id : {A : Set} → A → A
id = λ z → z

transport : ∀ {A : Set} {P : A → Set} {x y : A} (p : x ≡ y)  → P x → P y
transport {A} {P} {x} {y} = J D d x y
  where
    D : (x y : A) → x ≡ y → Set
    D x y p =  P x → P y
    d : (x : A) → D x x r
    d = λ x → id

p* : {A : Set} {P : A → Set} {x : A} {y : A} {p : x ≡ y} → P x → P y
-- p* {P = P} {p = p} u = transport P p u
p* {P = P} {p = p} u = transport p u

_* : {A : Set} {P : A → Set} {x : A} {y : A} (p : x ≡ y) → P x → P y
(p *) u = transport p u
-- p * u = transport p u

apd : {A : Set} {P : A → Set} (f : (x : A) → P x) {x y : A} {p : x ≡ y}
  → p* {P = P} {p = p} (f x) ≡ f y
apd {A} {P} f {x} {y} {p} = J D d x y p
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = p* {P = P} {p = p} (f x) ≡ f y
    d : (x : A) → D x x r
    d = λ x → r

_×_ : Set → Set → Set
A × B = Σ A (λ _ → B)

-- 2.6.1
fprodId : {A B : Set} {x y : A × B} → _≡_ {A × B} x y → ((fst x) ≡ (fst y)) × ((snd x) ≡ (snd y))
fprodId p = (apf fst p) , (apf snd p)
-- fprodId r = r , r

-- 2.6.4
-- alternative name consistent with book, A×B
×fam : {Z : Set} {A B : Z → Set} → (Z → Set)
×fam {A = A} {B = B} z = A z × B z

transport× : {Z : Set} {A B : Z → Set} {z w : Z} (p : z ≡ w) (x : ×fam {Z} {A} {B} z) → (transport p x ) ≡ (transport {Z} {A} p (fst x) , transport {Z} {B} p (snd x))
transport× r s = r

fprod : {A B A' B' : Set} (g : A → A') (h : B → B') → (A × B → A' × B')
fprod g h x = g (fst x) , h (snd x)

-- inverse of fprodId
pair= : {A B : Set} {x y : A × B} → (fst x ≡ fst y) × (snd x ≡ snd y) → x ≡ y
pair= (r , r) = r

-- 2.6.5
functorProdEq : {A B A' B' : Set} (g : A → A') (h : B → B')  (x y : A × B) (p : fst x ≡ fst y) (q : snd x ≡ snd y) →  apf (λ - → fprod g h -) (pair= (p , q)) ≡ pair= (apf g p , apf h q)
functorProdEq g h (a , b) (.a , .b) r r = r


  
-- 2.7.3
etaDprod : {A : Set} {P : A → Set} (z : Σ A (λ x → P x)) → z ≡ (fst z , snd z)
etaDprod z = r

-- 2.7.4
Σfam : {A : Set} {P : A → Set} (Q : Σ A (λ x → P x) → Set) → (A → Set)
Σfam {P = P} Q x = Σ (P x) λ u → Q (x , u) 

dpair= : {A : Set} {P : A → Set} {w1 w1' : A} {w2 : P w1 } {w2' : P w1'} →  (p : Σ (w1 ≡ w1') (λ p → p* {p = p} w2 ≡ w2')) → (w1 , w2) ≡ (w1' , w2')
dpair= (r  , r) = r

transportΣ : {A : Set} {P : A → Set} (Q : Σ A (λ x → P x) → Set) (x y : A) (p : x ≡ y) ((u , z) : Σfam Q x)
             →  _* {P = λ - → Σfam Q - } p (u , z) ≡ ((p *) u  , _* {P = λ - → Q ((fst -) , (snd -))} (dpair= (p , r)) z)
transportΣ Q x .x r (u , z) = r -- some agda bug here.  try ctrl-c ctrl-a

fDprod : {A A' : Set} {P : A → Set} {Q : A' → Set} (g : A → A') (h : (a : A) →  P a → Q (g a)) → (Σ A λ a → P a) → (Σ A' λ a' → Q a')
fDprod g h (a , pa) = g a , h a pa

ap2 : {A B C : Set} {x x' : A} {y y' : B} (f : A → B → C)
      → (x ≡ x') → (y ≡ y') → (f x y ≡ f x' y')
ap2 f r r = r

apd' : {A : Set} {P : A → Set} (f : (x : A) → P x) {x y : A} {p : x ≡ y}
  → p* {P = P} {p = p} (f x) ≡ {!f y!}
  -- →  (f x) ≡ {!!}
apd' = {!!}

ap2d : {A : Set} {x x' : A}  {P : A → Set} {y : P x} {y' : P x'} {C : (x : A)
  → P x → Set} (f : (x : A) → (y : P x) → C x y )
  → (p : x ≡ x') → (q : (p *) y ≡ y') →
  p* {p = p} f x y ≡ {!!}
  -- p* {p = q} (p* {p = p} (f x)) y ≡ {!f x' y'!}
  -- (f x y ≡ f x' y')
ap2d = {!!}

-- (.patternInTele0 .patternInTele1 : Σ A P)

functorDProdEq : {A A' : Set} {P : A → Set} {Q : A' → Set} (g : A → A') 
                 (h : (a : A) →  P a → Q (g a))
                 → ((x1 , y1) (x2 , y2) : Σ A λ a → P a)
                 → (p : x1 ≡ x2) (q : p* {p = p} y1 ≡ y2)
                 → apf (λ - → fDprod g h -) (dpair= (p , q))
                 ≡ dpair= ((apf g p , {!apd (ap2 h ? ?)!} ))
functorDProdEq = {!!}
1
typesagdadependent-typehomotopy-type-theory

1 Answers

1
votes

As a partial answer, I was able to refactor with a new transportd function via Escardo's notes, which makes everything explicit. Nonetheless, I still find it a bit confusing what is actually happening.

transportd : {X : Set } (A : X → Set  ) (B : (x : X) → A x → Set )
  {x : X} ((a , b) : Σ (A x) λ a → B x a) {y : X} (p : x ≡ y)
  → B x a → B y (transport {P = A} p a)
transportd A B (a , b) r = id

ap2d : {A : Set} {x x' : A}  {P : A → Set} {y : P x} {y' : P x'} {C : (x : A)
  → P x → Set} (f : (x : A) → (y : P x) → C x y )
  → (p : x ≡ x') → (q : p* {P = P} {p = p} y ≡ y') → 
  p* {P = C x'} {p = q} (transportd P C (y , (f x y)) p (f x y)) ≡ f x' y'
ap2d f r r = r

Regarding the .patternInTele1 pattern, I was able to remediate this by not pattern matching in the type signature but instead calling the fst and snd constructors, so that the context now looks like

Goal: p* (h (fst x) (snd x)) ≡ h (fst y) (snd y)
————————————————————————————————————————————————————————————
q  : p* (snd x) ≡ snd y
p  : fst x ≡ fst y
y  : Σ A (λ a → P a)
x  : Σ A (λ a → P a)
h  : (a : A) → P a → Q (g a)
g  : A → A'
Q  : A' → Set
P  : A → Set
A' : Set
A  : Set
———— Constraints ———————————————————————————————————————————
_2596 := (_ : _P_2595) y : _A_2583

where the new functorDProdEq is :

functorDProdEq : {A A' : Set} {P : A → Set} {Q : A' → Set} (g : A → A') 
                 (h : (a : A) →  P a → Q (g a))
                 → (x y : Σ A λ a → P a)
                 → (p : fst x ≡ fst y) (q : p* {p = p} (snd x) ≡ snd y)
                 → apf (λ - → fDprod {P = P} {Q = Q} g h -) (dpair= (p , q))
                 ≡ dpair= (apf g p , ? )
functorDProdEq = {!!}

I'm still having problems, as it won't allow me to fill this final hole. If I replace the question mark with ap2d h p q it highlights the last two lines yellow, and says

P (fst y) != A' of type Set
when checking that the expression ap2d h p q has type
p* (h (fst x) (snd x)) ≡ h (fst y) (snd y)

I still find the agda error messages unreadable, specifically the != * of type Set. Are there any resources to understand this? If instead, I try to fill the hole in step by step, it wont let me pattern match either p or q, as in ap2d h p {!q!} gives

Goal: p* _y_2654 ≡ snd y
Have: p* (snd x) ≡ snd y

Which seems like it should be correct? What am I missing?

Additionally, is it advisable to never pattern match in a typing context if you are reasoning about the type youre building (I know its generally bad practice to try to define types you don't understand, but I'm doing so for the sake of this exercise.)