(** ** raw matrices Raw matrices of a map are formed from a product decomposition of the target or from a sum decomposition of the source. We call them "raw" to distinguish them from matrices formed from direct sum decompositions. *) Require Import UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.RepresentableFunctors.Representation UniMath.CategoryTheory.RepresentableFunctors.Precategories. Local Open Scope cat. Definition to_row {C:category} {I} {b:I -> ob C} (B:Sum b) {d:ob C} : (Hom C (universalObject B) d) ≃ (∏ j, Hom C (b j) d). Proof. intros. exact (universalProperty B d). Defined. Definition from_row {C:category} {I} {b:I -> ob C} (B:Sum b) {d:ob C} : (∏ j, Hom C (b j) d) ≃ (Hom C (universalObject B) d). Proof. intros. apply invweq. apply to_row. Defined. Lemma from_row_entry {C:category} {I} {b:I -> ob C} (B:Sum b) {d:ob C} (f : ∏ j, Hom C (b j) d) : ∏ j, from_row B f ∘ opp_mor (universalElement B j) = f j. Proof. intros. exact (eqtohomot (homotweqinvweq (to_row B) f) j). Qed. Definition to_col {C:category} {I} {d:I -> ob C} (D:Product d) {b:ob C} : (Hom C b (universalObject D)) ≃ (∏ i, Hom C b (d i)). Proof. intros. exact (universalProperty D b). Defined. Definition from_col {C:category} {I} {d:I -> ob C} (D:Product d) {b:ob C} : (∏ i, Hom C b (d i)) ≃ (Hom C b (universalObject D)). Proof. intros. apply invweq. apply to_col. Defined. Lemma from_col_entry {C:category} {I} {b:I -> ob C} (D:Product b) {d:ob C} (f : ∏ i, Hom C d (b i)) : ∏ i, universalElement D i ∘ from_col D f = f i. Proof. intros. apply (eqtohomot (homotweqinvweq (to_col D) f ) i). Qed. Definition to_matrix {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) : (Hom C (universalObject B) (universalObject D)) ≃ (∏ i j, Hom C (b j) (d i)). Proof. intros. apply @weqcomp with (Y := ∏ i, Hom C (universalObject B) (d i)). { apply to_col. } { apply weqonsecfibers; intro i. apply to_row. } Defined. Definition from_matrix {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) : weq (∏ i j, Hom C (b j) (d i)) (Hom C (universalObject B) (universalObject D)). Proof. intros. apply invweq. apply to_matrix. Defined. Lemma from_matrix_entry {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) (f : ∏ i j, Hom C (b j) (d i)) : ∏ i j, (universalElement D i ∘ from_matrix D B f) ∘ opp_mor (universalElement B j) = f i j. Proof. intros. exact (eqtohomot (eqtohomot (homotweqinvweq (to_matrix D B) f) i) j). Qed. Lemma from_matrix_entry_assoc {C:category} {I} {d:I -> ob C} (D:Product d) {J} {b:J -> ob C} (B:Sum b) (f : ∏ i j, Hom C (b j) (d i)) : ∏ i j, universalElement D i ∘ (from_matrix D B f ∘ opp_mor(universalElement B j)) = f i j. Proof. intros. rewrite <- assoc. exact (from_matrix_entry D B f i j). Qed.