It's true that in intuitionistic logic "A implies (A or B)"; the usual computational interpretation of that is that "there is a function taking a value of type A and returning a value of type A + B", where + is the tagged union, and, per above, that function is exactly the one which tags its input as belonging to the left disjunct.

I suspect you are still reading "A implies B" as "A is a subtype of B", derived from a set-theoretic interpretation of propositional logic. But the constructive interpretation is that a proof of "A implies B" is a method to take a proof of A and transform it into a proof of B. Computationally, a value of type "A implies B" (typically rewritten "A -> B") is a function that takes values of type A and returns values of type B.

Well, everything I've said here is standard and widely-taught; go forth and check if you're inclined to. A good introduction is the one by Philip Wadler, https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as... (tagged unions appear in Section 3, though it's all worth reading). A much more to-the-point and programming-focused account is in this OCaml book: https://cs3110.github.io/textbook/chapters/adv/curry-howard.... (very little OCaml syntax is used). You can find countless more.