diff --git a/doc/Doc.autodoc b/doc/Doc.autodoc
index a2f1774..db56c0e 100644
--- a/doc/Doc.autodoc
+++ b/doc/Doc.autodoc
@@ -58,6 +58,9 @@
 @Subsection Lift
 @InsertChunk Lift
 
+@Subsection Colift
+@InsertChunk Colift
+
 @Subsection Singleton morphism
 @InsertChunk SingletonMorphism
 
diff --git a/examples/Colift.g b/examples/Colift.g
new file mode 100644
index 0000000..b02edd5
--- /dev/null
+++ b/examples/Colift.g
@@ -0,0 +1,30 @@
+#! @Chunk Colift
+
+LoadPackage( "FinSetsForCAP" );
+
+#! @Example
+m := FinSet( [ 1 .. 5 ] );
+#! <An object in FinSets>
+n := FinSet( [ 1 .. 4 ] );
+#! <An object in FinSets>
+f := MapOfFinSets(
+             m,
+             [ [ 1, 2 ], [ 2, 2 ], [ 3, 1 ], [ 4, 1 ], [ 5, 3 ] ],
+             n );
+#! <A morphism in FinSets>
+g := MapOfFinSets(
+             m,
+             [ [ 1, 5 ], [ 2, 5 ], [ 3, 4 ], [ 4, 4 ], [ 5, 5 ] ],
+             m );
+#! <A morphism in FinSets>
+IsColiftable( f, g );
+#! true
+chi := Colift( f, g );
+#! <A morphism in FinSets>
+Display( chi );
+#! [ [ 1 .. 4 ], [ [ 1, 4 ], [ 2, 5 ], [ 3, 5 ], [ 4, 1 ] ], [ 1 .. 5 ] ]
+PreCompose( f, Colift( f, g ) ) = g;
+#! true
+IsColiftable( g, f );
+#! false
+#! @EndExample
diff --git a/gap/FinSets.gd b/gap/FinSets.gd
index 16a0c11..109afb3 100644
--- a/gap/FinSets.gd
+++ b/gap/FinSets.gd
@@ -222,6 +222,13 @@ DeclareOperation( "ProjectionOfFinSets",
 DeclareOperation( "Preimage",
         [ IsMorphismInCategoryOfFiniteSets, IsObjectInCategoryOfFiniteSets ] );
 
+#! @Description
+#!  Compute an element of the preimage of the element <A>y</A> under the morphism <A>f</A>.
+#! @Arguments f, y
+#! @Returns a GAP object
+DeclareOperation( "ElementOfPreimage",
+        [ IsMorphismInCategoryOfFiniteSets, IsObject ] );
+
 #! @Description
 #!  Compute the image of <A>S_</A> under the morphism <A>f</A>.
 #! @Arguments f, S_
diff --git a/gap/FinSets.gi b/gap/FinSets.gi
index c886082..c5183f8 100644
--- a/gap/FinSets.gi
+++ b/gap/FinSets.gi
@@ -374,6 +374,17 @@ InstallMethod( Preimage,
     
 end );
 
+##
+InstallMethod( ElementOfPreimage,
+        "for a CAP map of finite sets and a GAP object",
+        [ IsMorphismInCategoryOfFiniteSets, IsObject ],
+        
+  function ( f, y )
+    
+    return First( Source( f ), x -> IsEqualForElementsOfFinSets( f(x), y ) );
+    
+end );
+
 ##
 InstallMethod( ImageObject,
         "for a CAP map of finite sets and a CAP finite set",
@@ -785,6 +796,42 @@ AddLift( category_of_finite_sets,
     
 end );
 
+## beta \circ alpha^{-1} is again an ordinary function,
+## i.e., fibers of alpha are mapped under beta to the same element
+AddIsColiftable( category_of_finite_sets,
+  function ( category_of_finite_sets, alpha, beta )
+    
+    return ForAll( AsList( ImageObject( alpha ) ),
+                   i -> Length( DuplicateFreeList( List( Preimage( alpha, FinSetNC( category_of_finite_sets, [ i ] ) ), beta ) ) ) = 1 );
+    
+end );
+
+##
+AddColift( category_of_finite_sets,
+  function ( category_of_finite_sets, alpha, beta )
+    local S, T, im_alpha, elm_T, chi;
+    
+    S := Range( alpha );
+    T := Range( beta );
+    
+    im_alpha := AsList( ImageObject( alpha ) );
+    
+    if not IsInitial( T ) then ## this is, e.g., implied by not IsInitial( S ), since we assume a colift exists
+        elm_T := AsList( T )[1];
+    fi;
+    
+    chi :=
+      function ( y )
+        if not y in im_alpha then
+            return [ y, elm_T ];
+        fi;
+        return [ y, beta( ElementOfPreimage( alpha, y ) ) ];
+    end;
+    
+    return MapOfFinSets( S, List( AsList( S ), chi ), T );
+    
+end );
+
 ##
 AddImageEmbedding( category_of_finite_sets,
   function ( category_of_finite_sets, phi )