`inl : β―βΊ β πΈ β
`inl = val β¨ x β© `pair `Β· `true `Β· x
`inr : β―βΊ β πΈ β
`inr = val β¨ x β© `pair `Β· `false `Β· x
`match : β―βΊ β πΈ β
`match = val β¨ f β© β¨ g β© β¨ s β© `fst `Β· s `Β· f `Β· g `Β· (`snd `Β· s)
abstract
`inlββ : β x β β β `inl β x β
`inlββ {x} hx = subst β_β (sym (abs-Ξ² _ [] (x , hx))) (`pairββ (`true .snd) hx)
`inrββ : β x β β β `inr β x β
`inrββ {x} hx = subst β_β (sym (abs-Ξ² _ [] (x , hx))) (`pairββ (`false .snd) hx)
`matchββ : β f β β β g β β β `match β f β g β
`matchββ {f = f} {g} hf hg = subst β_β (sym (abs-Ξ²β [] ((g , hg) β· (f , hf) β· []))) (absβ _ _)
`match-Ξ²l
: β x β β β f β β β g β
β `match β f β g β (`inl β x) β‘ f β x
`match-Ξ²l {x = x} {f} {g} hx hf hg =
`match β f β g β (`inl β x) β‘β¨ abs-Ξ²β [] ((`inl β x , `inlββ hx) β· (g , hg) β· (f , hf) β· []) β©
`fst β β `inl β x β β f β g β (`snd β β `inl β x β) β‘β¨ ap! (abs-Ξ² _ [] (x , hx)) β©
`fst β (`pair β `true β x) β f β g β (`snd β (`pair β `true β x)) β‘β¨ apβ (Ξ» e p β e % f % g % p) (`fst-Ξ² (`true .snd) hx) (`snd-Ξ² (`true .snd) hx) β©
`true β f β g β x β‘β¨ ap (Ξ» e β e β x) (`true-Ξ² hf hg) β©
f β x β
`match-Ξ²r
: β x β β β f β β β g β
β `match β f β g β (`inr β x) β‘ g β x
`match-Ξ²r {x = x} {f} {g} hx hf hg =
`match β f β g β (`inr β x) β‘β¨ abs-Ξ²β [] ((`inr β x , `inrββ hx) β· (g , hg) β· (f , hf) β· []) β©
`fst β β `inr β x β β f β g β (`snd β β `inr β x β) β‘β¨ ap! (abs-Ξ² _ [] (x , hx)) β©
`fst β (`pair β `false β x) β f β g β (`snd β (`pair β `false β x)) β‘β¨ apβ (Ξ» e p β e % f % g % p) (`fst-Ξ² (`false .snd) hx) (`snd-Ξ² (`false .snd) hx) β©
`false β f β g β x β‘β¨ ap (Ξ» e β e β x) (`false-Ξ² hf hg) β©
g β x β