school/type-theory

Fork 0

Path between fibers for boolean equivalence #2

New issue

Closed

opened 2023-05-08 23:56:50 +00:00 by michael · 2 comments

michael commented

2023-05-08 23:56:50 +00:00

Owner

Files

Current status

Can't really figure out what the values to use for path induction yet, stuck at an error about using px inside my induction type. See latest posts for details

References:

https://1lab.dev/1Lab.Equiv.html#2570
- TODO: How does this (~ i ∨ j) work?

### Files - [bool equiv (cubical)][1] - [bool equiv (non cubical)][2] [1]: https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-06-equiv.lagda.md [2]: https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-17-equiv-no-cubical.agda ### Current status Can't really figure out what the values to use for path induction yet, stuck at an error about using `px` inside my induction type. See latest posts for details ### References: - https://1lab.dev/1Lab.Equiv.html#2570 - TODO: How does this `(~ i ∨ j)` work?

michael started working 2023-05-09 02:06:10 +00:00

michael stopped working 2023-05-09 02:31:43 +00:00

25 minutes 33 seconds

michael commented

2023-05-15 19:33:46 +00:00

Author

Owner

Trying this again in this file

I feel like the answer here was I'm trying to make fx and fz ≡ each other:

convert-fiber-is-contr : (y : Other) → (fz : fiber convert y) → convert-fiber y ≡ fz
convert-fiber-is-contr y fz i =
  let
    fx : fiber convert y
    fx = convert-fiber y

So fx is the fiber that we have, or the center, and then fz is some other fiber that we're comparing to. The problem is, Agda seems to think that these fibers aren't the same type?

fst fz != fst (convert-fiber y) of type Bool
when checking that the expression sfz has type
convert (fst (convert-fiber y)) ≡ y

Trying this again in [this file](https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-15-equiv-try-again.agda) I feel like the answer here was I'm trying to make fx and fz ≡ each other: ``` convert-fiber-is-contr : (y : Other) → (fz : fiber convert y) → convert-fiber y ≡ fz convert-fiber-is-contr y fz i = let fx : fiber convert y fx = convert-fiber y ``` So fx is the fiber that we have, or the center, and then fz is some other fiber that we're comparing to. The problem is, Agda seems to think that these fibers aren't the same type? ``` fst fz != fst (convert-fiber y) of type Bool when checking that the expression sfz has type convert (fst (convert-fiber y)) ≡ y ```

michael added the

asking-favonia

label 2023-05-15 19:34:39 +00:00

michael removed the

asking-favonia

label 2023-05-15 21:41:08 +00:00

michael added this to the (deleted) project 2023-05-15 23:26:49 +00:00

michael commented

2023-05-17 09:00:21 +00:00

Author

Owner

( associated commit: 98c5b14e06 )

ok going to try this again without cubical in this doc

using path induction, I was able to get a bit closer. I cleared up what the goal type actually comes out to:

-- Goal type:
--  transport (λ cx → convert cx ≡ y)
--  (
--    sym (convert-inv-id x)
--    ∙ ap convert-inv (px ∙ sym pz)
--    ∙ convert-inv-id z
--  )
--  (proj₂ (center-fiber y))  <-- this is just px
--  ≡ proj₂ fz                <-- this is just pz
Σ-≡,≡→≡ (x≡z , px≡pz)

and then now i'm trying to come up with a definition here:

-- Using subst here because that's what Σ-≡,≡→≡ uses
px≡pz : (subst P x≡z px) ≡ pz
px≡pz = J
  (λ b p′ →
    let
      x≡b : x ≡ b
      x≡b = ?

      convert-the : convert b ≡ y
      convert-the = ?
    in
    (subst P x≡b px) ≡ convert-the
  ) x≡z refl

problem

problem is, when i try to use the most obvious definition for convert-the:

convert-the : convert b ≡ y            
convert-the = sym (ap convert x≡b) ∙ px

it blows up with this error:

trans                                                            
(sym                                                             
 (J (λ y p → convert (proj₁ (center-fiber y₁)) ≡ convert y)      
  (?0 (b = (proj₁ fz))                                           
   (p′ =                                                         
    (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙            
     ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ 
     convert-inv-id (proj₁ fz))))                                
  refl))                                                         
(proj₂ (center-fiber y₁))                                        
!= proj₂ fz of type convert (proj₁ fz) ≡ y₁                      
when checking that the inferred type of an application           
  subst (λ b → convert b ≡ y₁)                                   
  (?0 (b = (proj₁ fz))                                           
   (p′ =                                                         
    (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙            
     ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ 
     convert-inv-id (proj₁ fz))))                                
  (proj₂ (center-fiber y₁))                                      
  ≡                                                              
  sym                                                            
  (ap convert                                                    
   (?0 (b = (proj₁ fz))                                          
    (p′ =                                                        
     (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙           
      ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙
      convert-inv-id (proj₁ fz)))))                              
  ∙ proj₂ (center-fiber y₁)                                      
matches the expected type                                        
  subst (λ b → convert b ≡ y₁)                                   
  (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙              
   ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙   
   convert-inv-id (proj₁ fz))                                    
  (proj₂ (center-fiber y₁))                                      
  ≡ proj₂ fz                                                     
~

even though it successfully type checked the holes before

( associated commit: 98c5b14e06755200ac770b1a8a6eb80d8e7300b9 ) ok going to try this again without cubical in [this doc][1] [1]: https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-17-equiv-no-cubical.agda using path induction, I was able to get a bit closer. I cleared up what the goal type actually comes out to: ``` -- Goal type: -- transport (λ cx → convert cx ≡ y) -- ( -- sym (convert-inv-id x) -- ∙ ap convert-inv (px ∙ sym pz) -- ∙ convert-inv-id z -- ) -- (proj₂ (center-fiber y)) <-- this is just px -- ≡ proj₂ fz <-- this is just pz Σ-≡,≡→≡ (x≡z , px≡pz) ``` and then now i'm trying to come up with a definition here: ``` -- Using subst here because that's what Σ-≡,≡→≡ uses px≡pz : (subst P x≡z px) ≡ pz px≡pz = J (λ b p′ → let x≡b : x ≡ b x≡b = ? convert-the : convert b ≡ y convert-the = ? in (subst P x≡b px) ≡ convert-the ) x≡z refl ``` ### problem problem is, when i try to use the most obvious definition for `convert-the`: ``` convert-the : convert b ≡ y convert-the = sym (ap convert x≡b) ∙ px ``` it blows up with this error: <details> ``` trans (sym (J (λ y p → convert (proj₁ (center-fiber y₁)) ≡ convert y) (?0 (b = (proj₁ fz)) (p′ = (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙ ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ convert-inv-id (proj₁ fz)))) refl)) (proj₂ (center-fiber y₁)) != proj₂ fz of type convert (proj₁ fz) ≡ y₁ when checking that the inferred type of an application subst (λ b → convert b ≡ y₁) (?0 (b = (proj₁ fz)) (p′ = (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙ ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ convert-inv-id (proj₁ fz)))) (proj₂ (center-fiber y₁)) ≡ sym (ap convert (?0 (b = (proj₁ fz)) (p′ = (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙ ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ convert-inv-id (proj₁ fz))))) ∙ proj₂ (center-fiber y₁) matches the expected type subst (λ b → convert b ≡ y₁) (sym (convert-inv-id (proj₁ (center-fiber y₁))) ∙ ap convert-inv (proj₂ (center-fiber y₁) ∙ sym (proj₂ fz)) ∙ convert-inv-id (proj₁ fz)) (proj₂ (center-fiber y₁)) ≡ proj₂ fz ~ ``` </details> even though it successfully type checked the holes before

michael added the

T-equivalence

label 2023-05-17 09:55:36 +00:00

michael closed this issue

2024-05-16 14:09:44 +00:00