/home/laney/.irssi/irclogs/Freenode/#agda.log-20170321

--- Day changed Mon Mar 20 2017
quchenI can’t seem to write a value of type20/03 07:25
quchenTypeOf : ∀ {α} {A : Set α} → (_ : A) → A20/03 07:25
quchenIs this impossible, or did I just miss the crux for doing so?20/03 07:25
quchenI imagine it would be useful to say »this maps to the type of this other value«.20/03 07:26
quchenFor example, there may be two different things that have the same type, and »foo : TypeOf bar« would assert that.20/03 07:27
comietekquchen: did you not want to return Set \alpha?20/03 09:00
quchencomietek: Did I?20/03 09:06
comietekDid you?20/03 09:07
quchenWhat 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
comietekCurrently you have written the type of id20/03 09:08
quchenThe type of id would map to »a«, not »A«, no?20/03 09:09
quchen>>> TypeOf : ∀ {α} {A : Set α} → (_ : A) → A20/03 09:09
quchen>>> id : ∀ {α} {A : Set α} → (a : A) → a20/03 09:09
quchenAlright, this typechecks: 20/03 09:10
quchenTypeOf : ∀ {α} {A : Set α} (_ : A) → Set α20/03 09:10
quchenTypeOf {A = A} _ = A20/03 09:10
quchenI guess I fell victim to the indiscernability of types and values once again, confusing A with its type Set α.20/03 09:11
quchenNow it’s clear: TypeOf should map stuff to types, and the type of types is Set (level).20/03 09:12
quchenThanks for the hint :-)20/03 09:12
quchenNow: back to writing transitivity in terms of induction on ≡. :-x20/03 09:13
comietekTransitivity of what?20/03 09:14
quchenEquality20/03 09:14
quchentrans-via-ind : ∀ {α} {A : Set α} {x y z : A} → x ≡ y → y ≡ z → x ≡ z20/03 09:14
quchenWhere induction on equality is quite a beast to be pasted into one line on IRC ;-) 20/03 09:15
quchenind-≡ : ∀ {α β} {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 p20/03 09:15
quchenind-≡ C c x .x refl = c x20/03 09:15
quchenInduction 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
quchenPoint 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
quchenSymmetry wasn’t so hard,20/03 09:19
quchensymm-via-ind : ∀ {α} {A : Set α} {x y : A} → x ≡ y → y ≡ x20/03 09:19
quchensymm-via-ind {x = x} {y = y} = ind-≡ (λ a₁ a₂ a₁≡a₂ → a₂ ≡ a₁) (λ _ → refl) x y20/03 09:19
comietekhm20/03 09:42
quchenanyway, I thought it would be cute to write »symm-via-ind : TypeOf symm«.20/03 09:57
quchenAnd not repeat this mess.20/03 09:57
comietekYou know you don't have to use J, right?20/03 10:00
quchencomietek: Oh no, without J it’s trivial20/03 10:01
quchenI just *want* to use J20/03 10:02
quchensymm refl = refl20/03 10:02
quchentrans refl refl = refl20/03 10:02
quchensubst P refl x = x20/03 10:02
quchenThat’s not the problem ;-)20/03 10:02
quchenHa! Subst works!20/03 10:03
quchensubst-via-ind {x = x} {y = y} p x≡y = ind-≡ (λ a₁ a₂ a₁≡a₂ → p a₁ → p a₂) (λ _ pa → pa) x y x≡y20/03 10:03
quchenThe crux was that »C x y p = p x -> p y«.20/03 10:04
quchenAnd that I should not separate the arrow into p x and p y, or something.20/03 10:04
gallaisIn 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
gallaisPlus 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 indices20/03 10:08
gallais(I meant to point at the Paulin-Mohring version)20/03 10:09
quchengallais: What do you mean with »fixed«?20/03 10:16
gallaiscf. the link i've posted20/03 10:25
quchengallais: Sounds like what HoTT calls »pointed path induction«, where one point of the equality is fixed20/03 11:34
Saizanthe two formulations are mutually derivable btw20/03 12:27

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