Theory Phi_BI.Unital_Homo

theory Unital_Homo
  imports Algebras
begin

section ‹Unital Homomorphism›

typedef (overloaded) ('a::one,'b::one) unital_homo
    = ‹Collect (homo_one :: ('a ⇒ 'b) ⇒ bool)›
  morphisms apply_unital_homo Unital_Homo
  by (rule exI[where x = ‹λ_. 1›]) (simp add:sep_mult_commute homo_one_def)

setup_lifting type_definition_unital_homo

lemmas unital_homo_inverse[simp] = Unital_Homo_inverse[simplified]

lemma apply_unital_homo_1[simp]: "apply_unital_homo I 1 = 1"
  using homo_one_def apply_unital_homo by blast

lemma unital_homo_eq_I[intro!]:
  ‹apply_unital_homo x = apply_unital_homo y ⟹ x = y›
  by (simp add: apply_unital_homo_inject)

lemma apply_unital_homo__homo_one:
  ‹homo_one (apply_unital_homo x)›
  by (simp add: homo_one_def)

lift_definition unital_homo_composition
    :: ‹('a::one,'b::one) unital_homo ⇒ ('c::one,'a) unital_homo ⇒ ('c,'b) unital_homo›
    (infixl "∘⇩U⇩H" 55)
  is ‹(o) :: ('a ⇒ 'b) ⇒ ('c ⇒ 'a) ⇒ ('c ⇒ 'b)›
  by (clarsimp simp add: homo_one_def)

notation unital_homo_composition (infixl "o⇩U⇩H" 55)

lemma apply_unital_homo_comp[simp]:
  ‹apply_unital_homo (f ∘⇩U⇩H g) = apply_unital_homo f o apply_unital_homo g›
  by (transfer; clarsimp)


end