--- Day changed Mon Mar 20 2017 | ||

quchen | I can’t seem to write a value of type | 20/03 07:25 |
---|---|---|

quchen | TypeOf : ∀ {α} {A : Set α} → (_ : A) → A | 20/03 07:25 |

quchen | Is this impossible, or did I just miss the crux for doing so? | 20/03 07:25 |

quchen | I imagine it would be useful to say »this maps to the type of this other value«. | 20/03 07:26 |

quchen | For example, there may be two different things that have the same type, and »foo : TypeOf bar« would assert that. | 20/03 07:27 |

comietek | quchen: did you not want to return Set \alpha? | 20/03 09:00 |

quchen | comietek: Did I? | 20/03 09:06 |

comietek | Did you? | 20/03 09:07 |

quchen | What I *want* to do is to write »foo : TypeOf bar«, meaning that foo and bar could be put into the same list, for example. | 20/03 09:08 |

comietek | Currently you have written the type of id | 20/03 09:08 |

quchen | The type of id would map to »a«, not »A«, no? | 20/03 09:09 |

quchen | >>> TypeOf : ∀ {α} {A : Set α} → (_ : A) → A | 20/03 09:09 |

quchen | >>> id : ∀ {α} {A : Set α} → (a : A) → a | 20/03 09:09 |

quchen | Alright, this typechecks: | 20/03 09:10 |

quchen | TypeOf : ∀ {α} {A : Set α} (_ : A) → Set α | 20/03 09:10 |

quchen | TypeOf {A = A} _ = A | 20/03 09:10 |

quchen | I guess I fell victim to the indiscernability of types and values once again, confusing A with its type Set α. | 20/03 09:11 |

quchen | Now it’s clear: TypeOf should map stuff to types, and the type of types is Set (level). | 20/03 09:12 |

quchen | Thanks for the hint :-) | 20/03 09:12 |

quchen | Now: back to writing transitivity in terms of induction on ≡. :-x | 20/03 09:13 |

comietek | Transitivity of what? | 20/03 09:14 |

quchen | Equality | 20/03 09:14 |

quchen | trans-via-ind : ∀ {α} {A : Set α} {x y z : A} → x ≡ y → y ≡ z → x ≡ z | 20/03 09:14 |

quchen | Where induction on equality is quite a beast to be pasted into one line on IRC ;-) | 20/03 09:15 |

quchen | ind-≡ : ∀ {α β} {A : Set α} → (C : (a₁ a₂ : A) → a₁ ≡ a₂ → Set β) → (c : (a : A) → C a a refl) → (x y : A) → (p : x ≡ y) → C x y p | 20/03 09:15 |

quchen | ind-≡ C c x .x refl = c x | 20/03 09:15 |

quchen | Induction on equality was one thing that always confused me in HoTT, and apparently it is not a HoTT thing, but MLTT has it as well (called »J«). | 20/03 09:16 |

quchen | Point being, I’d like to be able to understand equality better, hence I’d like to get more used to J. | 20/03 09:16 |

quchen | Symmetry wasn’t so hard, | 20/03 09:19 |

quchen | symm-via-ind : ∀ {α} {A : Set α} {x y : A} → x ≡ y → y ≡ x | 20/03 09:19 |

quchen | symm-via-ind {x = x} {y = y} = ind-≡ (λ a₁ a₂ a₁≡a₂ → a₂ ≡ a₁) (λ _ → refl) x y | 20/03 09:19 |

comietek | hm | 20/03 09:42 |

quchen | anyway, I thought it would be cute to write »symm-via-ind : TypeOf symm«. | 20/03 09:57 |

quchen | And not repeat this mess. | 20/03 09:57 |

comietek | You know you don't have to use J, right? | 20/03 10:00 |

quchen | comietek: Oh no, without J it’s trivial | 20/03 10:01 |

quchen | I just *want* to use J | 20/03 10:02 |

quchen | symm refl = refl | 20/03 10:02 |

quchen | trans refl refl = refl | 20/03 10:02 |

quchen | subst P refl x = x | 20/03 10:02 |

quchen | That’s not the problem ;-) | 20/03 10:02 |

quchen | Ha! Subst works! | 20/03 10:03 |

quchen | subst-via-ind {x = x} {y = y} p x≡y = ind-≡ (λ a₁ a₂ a₁≡a₂ → p a₁ → p a₂) (λ _ pa → pa) x y x≡y | 20/03 10:03 |

quchen | The crux was that »C x y p = p x -> p y«. | 20/03 10:04 |

quchen | And that I should not separate the arrow into p x and p y, or something. | 20/03 10:04 |

gallais | In J one of the base point is fixed though, isn't it? https://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/ | 20/03 10:07 |

gallais | Plus this gives a definition which is true to the idea that the value argument is a *parameter* of the equality type rather than both of them being indices | 20/03 10:08 |

gallais | (I meant to point at the Paulin-Mohring version) | 20/03 10:09 |

quchen | gallais: What do you mean with »fixed«? | 20/03 10:16 |

gallais | cf. the link i've posted | 20/03 10:25 |

quchen | gallais: Sounds like what HoTT calls »pointed path induction«, where one point of the equality is fixed | 20/03 11:34 |

Saizan | the two formulations are mutually derivable btw | 20/03 12:27 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!