Definition ExtMor2 (D1 D2 : @DTri PT) (f3 : Ob3 D1 --> Ob3 D2) (f4 : (AddEquiv1 Trans (Ob1 D1)) --> (AddEquiv1 Trans (Ob1 D2))) (H : f3 · Mor3 D2 = Mor3 D1 · f4) : ∥ TriMor D1 D2 ∥. Proof. set (D1' := InvRotDTri PT D1). set (D2' := InvRotDTri PT D2). set (Ext' := DExt PT D1' D2' (# (AddEquiv2 Trans) f3) (((AddEquivUnitIso Trans (Ob1 D1)) : PT⟦_, _⟧) · (# (AddEquiv2 Trans) f4) · inv_from_z_iso (AddEquivUnitIso Trans (Ob1 D2))) (ExtMor2_Comm D1 D2 f3 f4 H)). use (squash_to_prop Ext' (propproperty _)). intros Ext. set (Mor := TExtMor Ext). use hinhpr. use make_TriMor. - use make_MPMor. + use make_MPMorMors. * exact (MPMor2 Mor). * exact (MPMor3 Mor). * exact ((inv_from_z_iso (AddEquivCounitIso Trans (Ob3 D1))) · (# (AddEquiv1 Trans) (MPMor1 Mor)) · (AddEquivCounitIso Trans (Ob3 D2))). + use make_MPMorComms. * exact (MPComm2 Mor). * exact (ExtMor2_Comm2 D1 D2 Mor). - exact (ExtMor2_Comm3 D1 D2 Mor). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Categories.Abgr. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.CategoryTheory.FiveLemma.