Set Universe Polymorphism.Unset Strict Universe Declaration.Set Primitive Projections.Axiom Relation @{u} : Type @{u} -> Type @{u}.Inductive GraphQuotient {A : Type @{i}} (R : Relation A) : Type @{u} :=Arguments gq {A R} a.Axiom IsConnMap@{i} : forall {A B : Type @{i}}, (A -> B) -> Type @{i}.Definition class_of@{i k} {A : Type @{i}} (R : Relation @{i} A) : A -> GraphQuotient@{i k} R := gq.Axiom issurj_class_of : forall {A : Type } (R : Relation A), IsConnMap (class_of R).Type } : Type := BuildHomomorphismforall (s : σ), A s -> B s }.Arguments Homomorphism {σ}.Arguments BuildHomomorphism {σ A B} def_hom.Definition QuotientAlgebra {σ : Type } (A : σ -> Type ) (Φ : forall s, Relation (A s)) (s : σ) : Type :=Definition def_hom_quotient {σ} {A : σ -> Type } (Φ : forall s, Relation (A s)) (s : σ) (x : A s) :Definition hom_quotient {σ} {A : σ -> Type } (Φ : forall s, Relation (A s)) : Homomorphism A (QuotientAlgebra A Φ) :=Lemma surjection_quotient : forall {σ} {A : σ -> Type } (Φ : forall s, Relation (A s)) s, IsConnMap (def_hom (hom_quotient Φ) s).Proof .intros σ A Φ s.apply issurj_class_of.Qed .quality 100%
¤ Dauer der Verarbeitung: 0.2 Sekunden
¤ *© Formatika GbR, Deutschland
