Incorporate reverse-ap for proving equivalence

michael commented

2023-05-08 23:55:55 +00:00

Owner

The bool equiv problem requires us to give an equivalence between fibers. For two fibers r = (x, f x ≡ y) and r' = (x', f x' ≡ y), we need to compare point-wise (x against x'), and (f x ≡ y against f x' ≡ y). In my terminology, r is the "center" fiber of all the contractible fibers, and r' is the for-all other fibers that are being compared.

The crux of this proof comes from the fact that we can set both sides equal to y. When we have p1 = f x ≡ y and p2 = f x' ≡ y we can do f x ≡ f x'. The tricky step here is that in order to turn this into x ≡ x', we have to ap the inverse of f.

Normally you can't just "un-ap" a function but since we know we are working with equivalences we can get the inverse with the function f-inv y = x. But I don't think this actually works because this doesn't actually generalize automatically yet? Pending more investigation

The [bool equiv problem][1] requires us to give an equivalence between _fibers_. For two fibers `r = (x, f x ≡ y)` and `r' = (x', f x' ≡ y)`, we need to compare point-wise (x against x'), and (f x ≡ y against f x' ≡ y). In my terminology, `r` is the "center" fiber of all the contractible fibers, and `r'` is the for-all other fibers that are being compared. [1]: https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-06-equiv.lagda.md The crux of this proof comes from the fact that we can set both sides equal to `y`. When we have `p1 = f x ≡ y` and `p2 = f x' ≡ y` we can do `f x ≡ f x'`. The tricky step here is that in order to turn this into `x ≡ x'`, we have to `ap` the inverse of f. Normally you can't just "un-`ap`" a function but since we know we are working with equivalences we can get the inverse with the function `f-inv y = x`. But I don't think this actually works because this doesn't actually generalize automatically yet? Pending more investigation

michael started working 2023-05-09 01:48:50 +00:00

michael commented

2023-05-09 01:59:13 +00:00

Author

Owner

Ok I think I had a slight breakthrough with why I was getting this wrong. I had thought that for a function (f : A -> B) and particular (y : B), the fiber would be (y, f x ≡ y) because of the notation that I used, but this makes no sense: the y is already fixed.

The fiber is actually the (x : A), along with the f x ≡ y.

Ok I think I had a slight breakthrough with why I was getting this wrong. I had thought that for a function (f : A -> B) and particular (y : B), the fiber would be (y, f x ≡ y) because of the notation that I used, but this makes no sense: the y is already fixed. The fiber is actually the (x : A), along with the f x ≡ y.

michael stopped working 2023-05-09 02:04:49 +00:00

15 minutes 59 seconds

michael started working 2023-05-14 05:56:24 +00:00

michael commented

2023-05-14 06:39:11 +00:00

Author

Owner

Ok Favonia's hint is to compute "ap g p", and then concatenate it with a proof that g is the left-inverse of f

Trying with:

Bool-id-inv : Bool → Bool
Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst

Bool-id-inv-is-inv : (b : Bool) → Bool-id-inv (Bool-id b) ≡ b
Bool-id-inv-is-inv true =
    Bool-id-inv (Bool-id true)
  ≡⟨ refl ⟩
    Bool-id-inv true
  ≡⟨ refl ⟩
    (Bool-id-is-equiv .equiv-proof true .fst) .fst
  ≡⟨ ? ⟩
    (true , Bool-id-refl true) .fst
  ≡⟨ ? ⟩
    true
  ∎
Bool-id-inv-is-inv false = ?

This isn't accepting the first question mark there, even though I've defined:

Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y

Ok Favonia's hint is to compute "ap g p", and then concatenate it with a proof that g is the left-inverse of f Trying with: ``` Bool-id-inv : Bool → Bool Bool-id-inv b = (((Bool-id-is-equiv .equiv-proof) b) .fst) .fst Bool-id-inv-is-inv : (b : Bool) → Bool-id-inv (Bool-id b) ≡ b Bool-id-inv-is-inv true = Bool-id-inv (Bool-id true) ≡⟨ refl ⟩ Bool-id-inv true ≡⟨ refl ⟩ (Bool-id-is-equiv .equiv-proof true .fst) .fst ≡⟨ ? ⟩ (true , Bool-id-refl true) .fst ≡⟨ ? ⟩ true ∎ Bool-id-inv-is-inv false = ? ``` This isn't accepting the first question mark there, even though I've defined: ``` Bool-id-is-equiv .equiv-proof y .fst = y , Bool-id-refl y ```

michael stopped working 2023-05-14 06:39:46 +00:00

43 minutes 22 seconds

michael commented

2023-05-15 19:31:00 +00:00

Author

Owner

I think I got the idea, see this file

eqv5 : convert-inv (convert z) ≡ convert-inv (convert x)
eqv5 = ap convert-inv eqv4

eqv6 : z ≡ x
eqv6 = sym (convert-inv-id z) ∙ eqv5 ∙ convert-inv-id x

I got by with proving:

convert-inv-id : (b : Bool) → convert-inv (convert b) ≡ b
convert-inv-id true = refl
convert-inv-id false = refl

and then just applying this works

I think I got the idea, see [this file](https://git.mzhang.io/school/cubical/src/branch/master/src/2023-05-15-equiv-try-again.agda) ``` eqv5 : convert-inv (convert z) ≡ convert-inv (convert x) eqv5 = ap convert-inv eqv4 eqv6 : z ≡ x eqv6 = sym (convert-inv-id z) ∙ eqv5 ∙ convert-inv-id x ``` I got by with proving: ``` convert-inv-id : (b : Bool) → convert-inv (convert b) ≡ b convert-inv-id true = refl convert-inv-id false = refl ``` and then just applying this works

michael closed this issue

2023-05-15 19:31:00 +00:00

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

michael added the

T-equivalence

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

Incorporate reverse-ap for proving equivalence #1